update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma
index b88464a91c84a1188626beeb2767fb65acb26c5f..dc829088925c5831bbfbe448cd002928dbc9bff7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma
@@ -25,6 +25,6 @@ lemma pippo (p) (f):
 #p elim p -p
 [ #f <lift_rmap_empty <lift_rmap_empty <tr_pushs_zero
 | * [ #n ] #p #IH #f //
-  <lift_rmap_d_sn <lift_rmap_d_sn <depth_d
+  <lift_rmap_d_sn <lift_rmap_d_sn <depth_d_sn
   @(trans_eq … (IH …)) -IH