X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_eq.ma;h=0273a3eb88560a961ced247647283b95fa33cb85;hb=13584a37bbcde10e03c8a488f5b93e1e042da0a6;hp=3413b07db2743f8a44ad9ce24bc043e3ea7c6baf;hpb=2cc4eb5d0210be58286e028278852122dcb68052;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
index 3413b07db..0273a3eb8 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -55,6 +55,7 @@ lemma lift_path_append_sn (p) (f) (q):
       q●↑[f]p = ↑❨(λg,p. proj_path g (q●p)), f, p❩.
 #p @(path_ind_lift … p) -p // [ #n #l #p |*: #p ] #IH #f #q
 [ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
+| <lift_m_sn <lift_m_sn //
 | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
   <IH <IH -IH <list_append_rcons_sn //
 | <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn