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 0cd0158c05e16f3016b4af5e1f24c4f2a8f0d363..003b8d1ce8ed74e479393a001c15145d578fb3cc 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,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,7 +59,7 @@ 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 →
+      ∀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
@@ -67,7 +67,7 @@ lemma preterm_in_root_inv_lcons_iref:
 qed-.
 
 lemma preterm_in_root_inv_lcons_abst:
-      ∀t,p,l. l;p ϵ ▵𝛌.t →
+      ∀t,p,l. l◗p ϵ ▵𝛌.t →
       ∧∧ 𝗟 = l & p ϵ ▵t.
 #t #p #l * #q
 <list_append_lcons_sn * #r #Hr #H0 destruct
@@ -75,7 +75,7 @@ lemma preterm_in_root_inv_lcons_abst:
 qed-.
 
 lemma preterm_in_root_inv_lcons_appl:
-      ∀u,t,p,l. l;p ϵ ▵@u.t →
+      ∀u,t,p,l. l◗p ϵ ▵@u.t →
       ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
        | ∧∧ 𝗔 = l & p ϵ ▵t.
 #u #t #p #l * #q