X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Frdeq.ma;h=2e155d1ee3680677e3591429dba64fe49610c166;hp=8388e6875da0c987fbe132906d6ae9bba7258c25;hb=a454837a256907d2f83d42ced7be847e10361ea9;hpb=b4283c079ed7069016b8d924bbc7e08872440829

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma b/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma
index 8388e6875..2e155d1ee 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/rdeq.ma
@@ -31,8 +31,8 @@ interpretation
 
 (* Basic properties ***********************************************************)
 
-lemma frees_tdeq_conf_rdeq: ∀f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → ∀T2. T1 ≛ T2 →
-                            ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≘ f.
+lemma frees_tdeq_conf_rdeq: ∀f,L1,T1. L1 ⊢ 𝐅+⦃T1⦄ ≘ f → ∀T2. T1 ≛ T2 →
+                            ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅+⦃T2⦄ ≘ f.
 #f #L1 #T1 #H elim H -f -L1 -T1
 [ #f #L1 #s1 #Hf #X #H1 #L2 #_
   elim (tdeq_inv_sort1 … H1) -H1 #s2 #H destruct
@@ -65,12 +65,12 @@ lemma frees_tdeq_conf_rdeq: ∀f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → ∀T2. T1
 ]
 qed-.
 
-lemma frees_tdeq_conf: ∀f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≘ f →
-                       ∀T2. T1 ≛ T2 → L ⊢ 𝐅*⦃T2⦄ ≘ f.
+lemma frees_tdeq_conf: ∀f,L,T1. L ⊢ 𝐅+⦃T1⦄ ≘ f →
+                       ∀T2. T1 ≛ T2 → L ⊢ 𝐅+⦃T2⦄ ≘ f.
 /4 width=7 by frees_tdeq_conf_rdeq, sex_refl, ext2_refl/ qed-.
 
-lemma frees_rdeq_conf: ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≘ f →
-                       ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≘ f.
+lemma frees_rdeq_conf: ∀f,L1,T. L1 ⊢ 𝐅+⦃T⦄ ≘ f →
+                       ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅+⦃T⦄ ≘ f.
 /2 width=7 by frees_tdeq_conf_rdeq, tdeq_refl/ qed-.
 
 lemma tdeq_rex_conf (R): s_r_confluent1 … cdeq (rex R).