- equivalene of tc_lfxs and lex + lfeq proved

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
index 8a770328f0758d0c063c21648c4058cabbb20915..f55500bd119b0318715fc5adb76a6ce334909ef0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
@@ -28,10 +28,7 @@ interpretation
 interpretation
    "degree-based ranged equivalence (local environment)"
    'StarEqSn h o f L1 L2 = (lexs (cdeq_ext h o) cfull f L1 L2).
-(*
-definition lfdeq_transitive: predicate (relation3 lenv term term) ≝
-           λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≛[h, o, T1] L2 → R L1 T1 T2.
-*)
+
 (* Basic properties ***********************************************************)
 
 lemma frees_tdeq_conf_lexs: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T2. T1 ≛[h, o] T2 →
@@ -195,11 +192,3 @@ lemma lfdeq_fwd_flat_dx: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → L1 
 lemma lfdeq_fwd_dx: ∀h,o,I2,L1,K2. ∀T:term. L1 ≛[h, o, T] K2.ⓘ{I2} →
                     ∃∃I1,K1. L1 = K1.ⓘ{I1}.
 /2 width=5 by lfxs_fwd_dx/ qed-.
-
-(* Basic_2A1: removed theorems 10:
-              lleq_ind lleq_fwd_lref
-              lleq_fwd_drop_sn lleq_fwd_drop_dx
-              lleq_skip lleq_lref lleq_free
-              lleq_Y lleq_ge_up lleq_ge
-               
-*)