X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Flpss_cpss.ma;h=6c060f88f5af5808d1e1c387d0d88520df21287c;hb=713673ecf863cb6187291f016ed4490b12a03ac0;hp=0e23bfce582360fe5cc5dea95fb461c9f8809064;hpb=520d4370a540a98f5e5e1d85acfef0c982cc1e04;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma
index 0e23bfce5..6c060f88f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma
@@ -109,7 +109,7 @@ elim (IH … HV01 … HV02 … HL01 … HL02) //
 elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/
 qed-.
 
-theorem cpss_conf_lpss: lpx_sn_confluent cpss.
+theorem cpss_conf_lpss: lpx_sn_confluent cpss cpss.
 #L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*]
 [ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
   elim (cpss_inv_atom1 … H1) -H1
@@ -139,7 +139,7 @@ qed-.
 theorem cpss_conf: ∀L. confluent … (cpss L).
 /2 width=6 by cpss_conf_lpss/ qed-.
 
-theorem cpss_trans_lpss: lpx_sn_transitive cpss.
+theorem cpss_trans_lpss: lpx_sn_transitive cpss cpss.
 #L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*]
 [ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct
   elim (cpss_inv_atom1 … H1) -H1