integrating the framework with fle ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfdeq_lfdeq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma
index 2edd66b91710474d0e2364d90cd7252b1803fd4b..2fae91f3901c2fff1cd7d727966ba89365bc4834 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma
@@ -15,12 +15,16 @@
 include "basic_2/syntax/ext2_ext2.ma".
 include "basic_2/syntax/tdeq_tdeq.ma".
 include "basic_2/static/lfxs_lfxs.ma".
-include "basic_2/static/lfdeq.ma".
+include "basic_2/static/lfdeq_length.ma".
 
 (* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******)
 
 (* Advanced properties ******************************************************)
 
+(* Basic_2A1: uses: lleq_sym *)
+lemma lfdeq_sym: ∀h,o,T. symmetric … (lfdeq h o T).
+/3 width=3 by lfdeq_fle_comp, lfxs_sym, tdeq_sym/ qed-.
+
 (* Basic_2A1: uses: lleq_dec *)
 lemma lfdeq_dec: ∀h,o,L1,L2. ∀T:term. Decidable (L1 ≛[h, o, T] L2).
 /3 width=1 by lfxs_dec, tdeq_dec/ qed-.
@@ -46,7 +50,7 @@ theorem lfdeq_bind_void: ∀h,o,p,I,L1,L2,V,T.
 (* Basic_2A1: uses: lleq_trans *)
 theorem lfdeq_trans: ∀h,o,T. Transitive … (lfdeq h o T).
 #h #o #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2
-lapply (frees_tdeq_conf_lexs … Hf1 T … HL1) // #H0
+lapply (frees_tdeq_conf_lfdeq … Hf1 T … HL1) // #H0
 lapply (frees_mono … Hf2 … H0) -Hf2 -H0
 /5 width=7 by lexs_trans, lexs_eq_repl_back, tdeq_trans, ext2_trans, ex2_intro/
 qed-.