update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / reduction / dbfr_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
index fc67c5779640106caa7c7f49f6ea1a4d9299ee4c..1f5c35a851d9c29726a1af037bc105c0a6361480 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
@@ -16,7 +16,7 @@ include "delayed_updating/reduction/dbfr.ma".
 
 include "delayed_updating/substitution/fsubst_lift.ma".
 include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_constructors.ma".
+include "delayed_updating/substitution/lift_prototerm_constructors.ma".
 include "delayed_updating/substitution/lift_path_structure.ma".
 include "delayed_updating/substitution/lift_path_closed.ma".
 include "delayed_updating/substitution/lift_rmap_closed.ma".
@@ -48,6 +48,7 @@ theorem dbfr_lift_bi (f) (t1) (t2) (r):
   @iref_eq_repl
   @(subset_eq_canc_sn … (lift_term_grafted_S …))
   @lift_term_eq_repl_sn
+(* 🠢[f]p ≗ ⇂*[↑(m+n)]🠢[f](((p◖𝗔)●b)●𝗟◗q) *)
 (* Note: crux of the proof begins *)
   >lift_rmap_A_dx
   /2 width=2 by tls_succ_plus_lift_rmap_append_closed_bLq_dx/