update in delayed updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / preterm_constructors.ma

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 03394c5bf6349fe99c6ab14b648259bea5fe8334..852fa0a59f204028bec097b7d212fbb0c51e8568 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
@@ -21,15 +21,15 @@ include "delayed_updating/notation/functions/at_2.ma".
 (* CONSTRUCTORS FOR PRETERM *************************************************)
 
 definition preterm_node_0 (l): preterm ≝
-           λp. l;𝐞 = p.
+           λ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,8 +50,8 @@ interpretation
 (* Basic Inversions *********************************************************)
 
 lemma preterm_in_root_inv_lcons_oref:
-      ∀p,l,n. l;p ϵ▵ #n →
-      ∧∧ 𝗱❨n❩ = l & 𝐞 = p.
+      ∀p,l,n. l◗p ϵ ▵#n →
+      ∧∧ 𝗱n = l & 𝐞 = p.
 #p #l #n * #q
 <list_append_lcons_sn #H0 destruct -H0
 elim (eq_inv_list_empty_append … e0) -e0 #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/