X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Freduction%2Fdfr_lift.ma;h=b60bd708c681b172e2f4c4ebbfdc3b403abe2879;hb=b1c5b3370653db6e495bbf6b3799cba592746cdd;hp=71a599326aeef8a38fec6578e4382153ff7cca6b;hpb=e4328f6887dc0235d49d965a5ba44787b1754b80;p=helm.git

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 71a599326..b60bd708c 100644
--- 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