update in basic_2 and ground_2

[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 9784f34904ddc209745c628de2a3d92dee9894be..98b9314459dc725b63eb3a3a8b0784e806783d86 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
@@ -31,8 +31,8 @@ interpretation
 
 (* Basic properties ***********************************************************)
 
-lemma frees_tdeq_conf_lfdeq: â\88\80h,o,f,L1,T1. L1 â\8a¢ ð\9d\90\85*â¦\83T1â¦\84 â\89¡ f → ∀T2. T1 ≛[h, o] T2 →
-                             â\88\80L2. L1 â\89\9b[h, o, f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85*â¦\83T2â¦\84 â\89¡ f.
+lemma frees_tdeq_conf_lfdeq: â\88\80h,o,f,L1,T1. L1 â\8a¢ ð\9d\90\85*â¦\83T1â¦\84 â\89\98 f → ∀T2. T1 ≛[h, o] T2 →
+                             â\88\80L2. L1 â\89\9b[h, o, f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85*â¦\83T2â¦\84 â\89\98 f.
 #h #o #f #L1 #T1 #H elim H -f -L1 -T1
 [ #f #L1 #s1 #Hf #X #H1 #L2 #_
   elim (tdeq_inv_sort1 … H1) -H1 #s2 #d #_ #_ #H destruct
@@ -65,12 +65,12 @@ lemma frees_tdeq_conf_lfdeq: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T
 ]
 qed-.
 
-lemma frees_tdeq_conf: â\88\80h,o,f,L,T1. L â\8a¢ ð\9d\90\85*â¦\83T1â¦\84 â\89¡ f →
-                       â\88\80T2. T1 â\89\9b[h, o] T2 â\86\92 L â\8a¢ ð\9d\90\85*â¦\83T2â¦\84 â\89¡ f.
+lemma frees_tdeq_conf: â\88\80h,o,f,L,T1. L â\8a¢ ð\9d\90\85*â¦\83T1â¦\84 â\89\98 f →
+                       â\88\80T2. T1 â\89\9b[h, o] T2 â\86\92 L â\8a¢ ð\9d\90\85*â¦\83T2â¦\84 â\89\98 f.
 /4 width=7 by frees_tdeq_conf_lfdeq, lexs_refl, ext2_refl/ qed-.
 
-lemma frees_lfdeq_conf: â\88\80h,o,f,L1,T. L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f →
-                        â\88\80L2. L1 â\89\9b[h, o, f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f.
+lemma frees_lfdeq_conf: â\88\80h,o,f,L1,T. L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f →
+                        â\88\80L2. L1 â\89\9b[h, o, f] L2 â\86\92 L2 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f.
 /2 width=7 by frees_tdeq_conf_lfdeq, tdeq_refl/ qed-.
 
 lemma tdeq_lfxs_conf: ∀R,h,o. s_r_confluent1 … (cdeq h o) (lfxs R).