]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma
renaming
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfdeq_fqup.ma
index 78320e1b19155f1701eb0bcb82a8f7f496012c41..c39dd5bbc77b5d01b02b525544a3eb2473d0c038 100644 (file)
@@ -19,7 +19,6 @@ include "basic_2/static/lfdeq.ma".
 
 (* Advanced properties ******************************************************)
 
-(* Basic_2A1: uses: lleq_refl *)
 lemma lfdeq_refl: ∀h,o,T. reflexive … (lfdeq h o T).
 /2 width=1 by lfxs_refl/ qed.