X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpreterm_constructors.ma;h=0cd0158c05e16f3016b4af5e1f24c4f2a8f0d363;hb=9605ffc88831066a901ea4eb8e419f277662f372;hp=03394c5bf6349fe99c6ab14b648259bea5fe8334;hpb=3c257bf84769adf162510ed86a89872e3003629a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
index 03394c5bf..0cd0158c0 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
@@ -24,12 +24,12 @@ definition preterm_node_0 (l): preterm ≝
            λp. l;𝐞 = p.
 
 definition preterm_node_1 (l): preterm → preterm ≝
-           λt,p. ∃∃q. q ϵ⬦ t & l;q = p.
+           λt,p. ∃∃q. q ϵ t & l;q = p.
 
 definition preterm_node_2 (l1) (l2): preterm → preterm → preterm ≝
            λt1,t2,p.
-           ∨∨ ∃∃q. q ϵ⬦ t1 & l1;q = p
-            | ∃∃q. q ϵ⬦ t2 & l2;q = p.
+           ∨∨ ∃∃q. q ϵ t1 & l1;q = p
+            | ∃∃q. q ϵ t2 & l2;q = p.
 
 interpretation
   "outer variable reference by depth (preterm)"
@@ -50,7 +50,7 @@ interpretation
 (* Basic Inversions *********************************************************)
 
 lemma preterm_in_root_inv_lcons_oref:
-      ∀p,l,n. l;p ϵ▵ #n →
+      ∀p,l,n. l;p ϵ ▵#n →
       ∧∧ 𝗱❨n❩ = l & 𝐞 = p.
 #p #l #n * #q
 <list_append_lcons_sn #H0 destruct -H0
@@ -59,25 +59,25 @@ elim (eq_inv_list_empty_append … e0) -e0 #H0 #_
 qed-.
 
 lemma preterm_in_root_inv_lcons_iref:
-      ∀t,p,l,n. l;p ϵ▵ 𝛗n.t →
-      ∧∧ 𝗱❨n❩ = l & p ϵ▵ t.
+      ∀t,p,l,n. l;p ϵ ▵𝛗n.t →
+      ∧∧ 𝗱❨n❩ = l & p ϵ ▵t.
 #t #p #l #n * #q
 <list_append_lcons_sn * #r #Hr #H0 destruct
 /3 width=2 by ex_intro, conj/
 qed-.
 
 lemma preterm_in_root_inv_lcons_abst:
-      ∀t,p,l. l;p ϵ▵ 𝛌.t →
-      ∧∧ 𝗟 = l & p ϵ▵ t.
+      ∀t,p,l. l;p ϵ ▵𝛌.t →
+      ∧∧ 𝗟 = l & p ϵ ▵t.
 #t #p #l * #q
 <list_append_lcons_sn * #r #Hr #H0 destruct
 /3 width=2 by ex_intro, conj/
 qed-.
 
 lemma preterm_in_root_inv_lcons_appl:
-      ∀u,t,p,l. l;p ϵ▵ @u.t →
-      ∨∨ ∧∧ 𝗦 = l & p ϵ▵ u
-       | ∧∧ 𝗔 = l & p ϵ▵ t.
+      ∀u,t,p,l. l;p ϵ ▵@u.t →
+      ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
+       | ∧∧ 𝗔 = l & p ϵ ▵t.
 #u #t #p #l * #q
 <list_append_lcons_sn * * #r #Hr #H0 destruct
 /4 width=2 by ex_intro, or_introl, or_intror, conj/