lsubs renamed as lsubr

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reducibility / cnf_cif.ma

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 8ee507cc14c1fa421326b2982f258bf56d0c79e3..5a1ae5a5b69050614d3ebbed20c1000ded88d228 100644 (file)
--- 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