update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / lift_eq.ma

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 3413b07db2743f8a44ad9ce24bc043e3ea7c6baf..0273a3eb88560a961ced247647283b95fa33cb85 100644 (file)
--- 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