Cerchiamo di costruire una deduzione in CL che abbia la formula
considerata come conclusione.

1. ksk = s                 (Axk)
2. kkk = k                 (Axk)
3. (ksk)(kkk)=(ksk)(kkk)   (assioma rifl)
4. (ksk)(kkk)=s(kkk)       (cong2)1.3.
5. (ksk)(kkk)=sk           (cong1)2.4.