X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpreterm_constructors.ma;h=003b8d1ce8ed74e479393a001c15145d578fb3cc;hb=503500ff9a6d9cca363a42b5fe7f3f5de69239f9;hp=0cd0158c05e16f3016b4af5e1f24c4f2a8f0d363;hpb=291fe1d3b56faf91d07099f43f3ebde2988649e1;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 0cd0158c0..003b8d1ce 100644
--- 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