(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpsss_ltpsss.ma".
-include "basic_2/reducibility/ltpr_ltpsss.ma".
+include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/reducibility/ltpr_ltpss.ma".
include "basic_2/reducibility/ltpr_ltpr.ma".
include "basic_2/reducibility/lcpr.ma".
lapply (ltpr_fwd_length … HK01) #H
>(ltpr_fwd_length … HK02) in H; #H
elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2
-lapply (ltpsss_fwd_length … HKL1) #H1
-lapply (ltpsss_fwd_length … HKL2) #H2
+lapply (ltpss_fwd_length … HKL1) #H1
+lapply (ltpss_fwd_length … HKL2) #H2
>H1 in HKL1 H; -H1 #HKL1
>H2 in HKL2; -H2 #HKL2 #H
-elim (ltpr_ltpsss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
-elim (ltpr_ltpsss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
-elim (ltpsss_conf … HK1 … HK2) -K #K #HK1 #HK2
+elim (ltpr_ltpss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
+elim (ltpr_ltpss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
+elim (ltpss_conf … HK1 … HK2) -K #K #HK1 #HK2
lapply (ltpr_fwd_length … HLK1) #H1
lapply (ltpr_fwd_length … HLK2) #H2
/3 width=5/