partial update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
index 71a599326aeef8a38fec6578e4382153ff7cca6b..b60bd708c681b172e2f4c4ebbfdc3b403abe2879 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
@@ -24,8 +24,6 @@ include "delayed_updating/substitution/lift_rmap_head.ma".
 
 (* Constructions with lift **************************************************)
 
-(* ↑[↑[p◖𝗔◖𝗟]f]q *)
-
 theorem dfr_lift_bi (f) (t1) (t2) (r):
         t1 ➡𝐝𝐟[r] t2 → ↑[f]t1 ➡𝐝𝐟[↑[f]r] ↑[f]t2.
 #f #t1 #t2 #r