X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freducibility%2Fcnf_cif.ma;h=5a1ae5a5b69050614d3ebbed20c1000ded88d228;hb=640716b0624d2a7cd9f339b9ab975e85b3288a50;hp=51ce95aa066356cb2f94e304e38727f00d6aa7b3;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
index 51ce95aa0..5a1ae5a5b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma
@@ -50,7 +50,7 @@ lemma tpr_cif_eq: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ 𝐈⦃T1⦄ → T1 = T2.
   elim (cif_inv_appl … H) -H #_ #_ #H
   elim (simple_inv_bind … H)
 | #a * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #L #H
-  [ lapply (tps_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+  [ lapply (tps_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
     elim (cif_inv_bind … H) -H #HV1 #HT1 * #H destruct
     lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
     lapply (IHT1 … HT1) -IHT1 #H destruct
@@ -96,7 +96,7 @@ lemma cnf_crf_false: ∀L,T. L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ⊥.
 | #a #L #V #W #T #H
   elim (cnf_inv_appl … H) -H #_ #_ #H
   elim (simple_inv_bind … H)
-| #a #L #V #W #T #H 
+| #a #L #V #W #T #H
   elim (cnf_inv_appl … H) -H #_ #_ #H
   elim (simple_inv_bind … H)
 ]