From a77d0bd6a04e94f765d329d47b37d9e04d349b14 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Thu, 3 May 2018 13:34:08 +0200
Subject: [PATCH] notational update in lambdadelta completed

+ minor improvements
---
 .../lambdadelta/alpha_1/syntax/term_append.ma |  2 +-
 .../apps_2/notation/models/downspoon_3.ma     |  6 +--
 .../lambdadelta/apps_2/web/apps_2.ldw.xml     |  7 ++++
 .../basic_2/relocation/lifts_vector.ma        | 18 ++++----
 .../basic_2/rt_computation/csx_cnx_vector.ma  |  2 +-
 .../basic_2/rt_computation/csx_csx_vector.ma  |  2 +-
 .../basic_2/rt_computation/csx_vector.ma      |  2 +-
 .../lambdadelta/basic_2/static/gcp_cr.ma      | 12 +++---
 .../lambdadelta/basic_2/syntax/append.ma      | 21 +++++-----
 .../basic_2/syntax/append_length.ma           | 12 +++---
 .../lambdadelta/basic_2/syntax/term_vector.ma |  2 +-
 .../ground_2/etc/lib/list2_append.etc         | 26 ++++++++++++
 .../append_2.ma => etc/lib/oplus_4.etc}       | 16 +++++--
 .../contribs/lambdadelta/ground_2/lib/list.ma | 12 +++---
 .../lambdadelta/ground_2/lib/list2.ma         | 16 ++-----
 .../lambdadelta/ground_2/lib/streams.ma       |  6 +--
 .../lambdadelta/ground_2/lib/streams_eq.ma    |  4 +-
 .../lambdadelta/ground_2/lib/streams_hdtl.ma  | 10 ++---
 .../lambdadelta/ground_2/lib/streams_tls.ma   |  4 +-
 .../notation/constructors/oplusright_5.ma     |  6 +--
 .../{downspoon_1.ma => downspoon_2.ma}        | 12 +++++-
 ...{downspoonstar_2.ma => downspoonstar_3.ma} | 12 +++++-
 .../lambdadelta/ground_2/relocation/mr2_at.ma | 12 +++---
 .../ground_2/relocation/mr2_minus.ma          | 18 ++++----
 .../ground_2/relocation/mr2_plus.ma           |  8 ++--
 .../ground_2/relocation/nstream.ma            | 16 +++----
 .../ground_2/relocation/nstream_after.ma      | 42 +++++++++----------
 .../ground_2/relocation/nstream_coafter.ma    | 20 ++++-----
 .../ground_2/relocation/nstream_eq.ma         |  6 +--
 .../ground_2/relocation/nstream_isid.ma       |  2 +-
 .../ground_2/relocation/nstream_istot.ma      | 14 +++----
 .../lambdadelta/ground_2/web/ground_2_src.tbl |  4 +-
 .../matita/contribs/lambdadelta/partial.txt   |  1 +
 33 files changed, 202 insertions(+), 151 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground_2/etc/lib/list2_append.etc
 rename matita/matita/contribs/lambdadelta/ground_2/{notation/functions/append_2.ma => etc/lib/oplus_4.etc} (73%)
 rename matita/matita/contribs/lambdadelta/ground_2/notation/functions/{downspoon_1.ma => downspoon_2.ma} (79%)
 rename matita/matita/contribs/lambdadelta/ground_2/notation/functions/{downspoonstar_2.ma => downspoonstar_3.ma} (74%)

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
index 4ea795a68..a2db5fedd 100644
--- a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
+++ b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
@@ -22,4 +22,4 @@ let rec tappend T U on T ≝ match T with
 | TPair I V T ⇒ ②{I}V.(tappend T U)
 ].
 
-interpretation "append (term)" 'Append T U = (tappend T U).
+interpretation "append (term)" 'plus T U = (tappend T U).
diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/downspoon_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/downspoon_3.ma
index 434c98e7e..a0e2b5fc3 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/notation/models/downspoon_3.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/downspoon_3.ma
@@ -16,12 +16,12 @@
 
 notation < "hvbox( â«°[ break term 46 i ] break term 46 lv )"
    non associative with precedence 46
-   for @{ 'DownSpoon $M $d $lv }.
+   for @{ 'DownSpoon $M $i $lv }.
 
 notation > "hvbox( â«°[ break term 46 i ] break term 46 lv )"
    non associative with precedence 46
-   for @{ 'DownSpoon ? $d $lv }.
+   for @{ 'DownSpoon ? $i $lv }.
 
 notation > "hvbox( â«°{ term 46 M }[ break term 46 i ] break term 46 lv )"
    non associative with precedence 46
-   for @{ 'DownSpoon $M $d $lv }.
+   for @{ 'DownSpoon $M $i $lv }.
diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
index a242c3124..8b3db76c3 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
@@ -13,6 +13,10 @@
          applications of λδ version 2.
          In particular it contains the components below.
    </body>
+   <topitem name="models">
+      <notice class="alpha" notice="Models."/>
+      Denotational semantics for λδ.
+   </topitem>
    <topitem name="MLTT1">
       <notice class="alpha" notice="MLTT1."/>
       Martin-Löf's Type Theory with one universe
@@ -33,6 +37,9 @@
          and its timeline.
    </body>
    <table name="apps_2_sum"/>
+   <news class="alpha" date="2018 April 30.">
+         The Models component is started for λδ version 2.
+   </news>
    <news class="alpha" date="2017 March 6.">
          The Examples component is moved from the Core directory.
    </news>
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
index 68cab8482..dc7c7d309 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
@@ -22,7 +22,7 @@ inductive liftsv (f:rtmap): relation (list term) ≝
 | liftsv_nil : liftsv f (◊) (◊)
 | liftsv_cons: ∀T1s,T2s,T1,T2.
                ⬆*[f] T1 ≘ T2 → liftsv f T1s T2s →
-               liftsv f (T1 @ T1s) (T2 @ T2s)
+               liftsv f (T1 ⨮ T1s) (T2 ⨮ T2s)
 .
 
 interpretation "uniform relocation (term vector)"
@@ -43,9 +43,9 @@ lemma liftsv_inv_nil1: ∀f,Y. ⬆*[f] ◊ ≘ Y → Y = ◊.
 /2 width=5 by liftsv_inv_nil1_aux/ qed-.
 
 fact liftsv_inv_cons1_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y →
-                           ∀T1,T1s. X = T1 @ T1s →
+                           ∀T1,T1s. X = T1 ⨮ T1s →
                            ∃∃T2,T2s. ⬆*[f] T1 ≘ T2 & ⬆*[f] T1s ≘ T2s &
-                                     Y = T2 @ T2s.
+                                     Y = T2 ⨮ T2s.
 #f #X #Y * -X -Y
 [ #U1 #U1s #H destruct
 | #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5 by ex3_2_intro/
@@ -53,9 +53,9 @@ fact liftsv_inv_cons1_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y →
 qed-.
 
 (* Basic_2A1: includes: liftv_inv_cons1 *)
-lemma liftsv_inv_cons1: ∀f:rtmap. ∀T1,T1s,Y. ⬆*[f] T1 @ T1s ≘ Y →
+lemma liftsv_inv_cons1: ∀f:rtmap. ∀T1,T1s,Y. ⬆*[f] T1 ⨮ T1s ≘ Y →
                         ∃∃T2,T2s. ⬆*[f] T1 ≘ T2 & ⬆*[f] T1s ≘ T2s &
-                                  Y = T2 @ T2s.
+                                  Y = T2 ⨮ T2s.
 /2 width=3 by liftsv_inv_cons1_aux/ qed-.
 
 fact liftsv_inv_nil2_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → Y = ◊ → X = ◊.
@@ -67,18 +67,18 @@ lemma liftsv_inv_nil2: ∀f,X. ⬆*[f] X ≘ ◊ → X = ◊.
 /2 width=5 by liftsv_inv_nil2_aux/ qed-.
 
 fact liftsv_inv_cons2_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y →
-                           ∀T2,T2s. Y = T2 @ T2s →
+                           ∀T2,T2s. Y = T2 ⨮ T2s →
                            ∃∃T1,T1s. ⬆*[f] T1 ≘ T2 & ⬆*[f] T1s ≘ T2s &
-                                     X = T1 @ T1s.
+                                     X = T1 ⨮ T1s.
 #f #X #Y * -X -Y
 [ #U2 #U2s #H destruct
 | #T1s #T2s #T1 #T2 #HT12 #HT12s #U2 #U2s #H destruct /2 width=5 by ex3_2_intro/
 ]
 qed-.
 
-lemma liftsv_inv_cons2: ∀f:rtmap. ∀X,T2,T2s. ⬆*[f] X ≘ T2 @ T2s →
+lemma liftsv_inv_cons2: ∀f:rtmap. ∀X,T2,T2s. ⬆*[f] X ≘ T2 ⨮ T2s →
                         ∃∃T1,T1s. ⬆*[f] T1 ≘ T2 & ⬆*[f] T1s ≘ T2s &
-                                  X = T1 @ T1s.
+                                  X = T1 ⨮ T1s.
 /2 width=3 by liftsv_inv_cons2_aux/ qed-.
 
 (* Basic_1: was: lifts1_flat (left to right) *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
index 9e0de4217..4a93b473e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
@@ -49,7 +49,7 @@ lemma csx_applv_sort: ∀h,o,G,L,s,Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Vs⦄ 
   #X #H #H0
   elim (cpxs_fwd_sort_vector … o … H) -H #H
   [ elim H0 -H0 //
-  | -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h s)))
+  | -H0 @(csx_cpxs_trans … (Ⓐ(V⨮Vs).⋆(next h s)))
     /3 width=1 by cpxs_flat_dx, deg_next_SO/
   ]
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
index 767ac4db6..d618a2437 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
@@ -67,7 +67,7 @@ lapply (csx_appl_theta … H … HW12) -H -HW12 #H
 lapply (csx_fwd_pair_sn … H) #HW1
 lapply (csx_fwd_flat_dx … H) #H1
 @csx_appl_simple_theq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2
-elim (cpxs_fwd_theta_vector … o … (V2@V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
+elim (cpxs_fwd_theta_vector … o … (V2⨮V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
 [ -H #H elim H2 -H2 //
 | -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma
index 6fdda2bbf..5d0552b95 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma
@@ -26,7 +26,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma csxv_inv_cons: ∀h,o,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T@Ts⦄ →
+lemma csxv_inv_cons: ∀h,o,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⨮Ts⦄ →
                      ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ ∧ ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Ts⦄.
 normalize // qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma
index 562169f0c..ae7140efe 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma
@@ -111,17 +111,17 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
 | #G #L #Vs #HVs #T #H1T #H2T #f #L0 #V0 #X #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
   lapply (s1 … IHB … HB) #HV0
-  @(s2 … IHA  … (V0@V0s)) /3 width=13 by cp0, gcp2_all, lifts_simple_dx, conj/
+  @(s2 … IHA  … (V0⨮V0s)) /3 width=13 by cp0, gcp2_all, lifts_simple_dx, conj/
 | #p #G #L #Vs #U #T #W #HA #f #L0 #V0 #X #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #X0 #HV0s #H0 #H destruct
   elim (lifts_inv_flat1 … H0) -H0 #U0 #X #HU0 #HX #H destruct
   elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
-  @(s3 … IHA … (V0@V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
+  @(s3 … IHA … (V0⨮V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
 | #G #L #Vs #HVs #s #f #L0 #V0 #X #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #X0 #HV0s #H0 #H destruct
   >(lifts_inv_sort1 … H0) -X0
   lapply (s1 … IHB … HB) #HV0
-  @(s4 … IHA … (V0@V0s)) /3 width=7 by gcp2_all, conj/
+  @(s4 … IHA … (V0⨮V0s)) /3 width=7 by gcp2_all, conj/
 | #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #f #L0 #V0 #X #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #X0 #HV0s #H0 #H destruct
   elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
@@ -133,13 +133,13 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
   elim (lifts_total W1 (𝐔❴↑j❵)) #W2 #HW12
   lapply (lifts_trans … HVW1 … HW12 ??) -HVW1 [3: |*: // ] #H
   lapply (lifts_conf … HV12 … H f ?) -V1 [ /2 width=3 by after_uni_succ_sn/ ] #HVW2
-  @(s5 … IHA … (V0@V0s) … HW12) /3 width=4 by drops_inv_gen, lifts_applv/
+  @(s5 … IHA … (V0⨮V0s) … HW12) /3 width=4 by drops_inv_gen, lifts_applv/
 | #G #L #V1s #V2s #HV12s #p #V #T #HA #HV #f #L0 #V10 #X #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V10s #X0 #HV10s #H0 #H destruct
   elim (lifts_inv_bind1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
   elim (lifts_total V10 (𝐔❴1❵)) #V20 #HV120
   elim (liftsv_total (𝐔❴1❵) V10s) #V20s #HV120s
-  @(s6 … IHA … (V10@V10s) (V20@V20s)) /3 width=7 by cp2, liftsv_cons/
+  @(s6 … IHA … (V10⨮V10s) (V20⨮V20s)) /3 width=7 by cp2, liftsv_cons/
   @(HA … (⫯f)) /3 width=2 by drops_skip, ext2_pair/
   [ @lifts_applv //
     lapply (liftsv_trans … HV10s … HV120s ??) -V10s [3: |*: // ] #H
@@ -150,7 +150,7 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
 | #G #L #Vs #T #W #HA #HW #f #L0 #V0 #X #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #X0 #HV0s #H0 #H destruct
   elim (lifts_inv_flat1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
-  @(s7 … IHA … (V0@V0s)) /3 width=5 by lifts_applv/
+  @(s7 … IHA … (V0⨮V0s)) /3 width=5 by lifts_applv/
 ]
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma
index 55e6e3472..b3a07339b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/functions/append_2.ma".
 include "basic_2/notation/functions/snitem_2.ma".
 include "basic_2/notation/functions/snbind1_2.ma".
 include "basic_2/notation/functions/snbind2_3.ma".
@@ -28,7 +27,7 @@ rec definition append L K on K ≝ match K with
 | LBind K I ⇒ (append L K).ⓘ{I}
 ].
 
-interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
+interpretation "append (local environment)" 'plus L1 L2 = (append L1 L2).
 
 interpretation "local environment tail binding construction (generic)"
    'SnItem I L = (append (LBind LAtom I) L).
@@ -49,18 +48,18 @@ interpretation "tail abstraction (local environment)"
    'SnAbst L T = (append (LBind LAtom (BPair Abst T)) L).
 
 definition d_appendable_sn: predicate (lenv→relation term) ≝ λR.
-                            ∀K,T1,T2. R K T1 T2 → ∀L. R (L@@K) T1 T2.
+                            ∀K,T1,T2. R K T1 T2 → ∀L. R (L+K) T1 T2.
 
 (* Basic properties *********************************************************)
 
-lemma append_atom: ∀L. L @@ ⋆ = L.
+lemma append_atom: ∀L. (L + ⋆) = L. (**) (* () should be redundant *)
 // qed.
 
 (* Basic_2A1: uses: append_pair *)
-lemma append_bind: ∀I,L,K. L@@(K.ⓘ{I}) = (L@@K).ⓘ{I}.
+lemma append_bind: ∀I,L,K. L+(K.ⓘ{I}) = (L+K).ⓘ{I}.
 // qed.
 
-lemma append_atom_sn: ∀L. ⋆@@L = L.
+lemma append_atom_sn: ∀L. ⋆ + L = L.
 #L elim L -L //
 #L #I >append_bind //
 qed.
@@ -69,25 +68,25 @@ lemma append_assoc: associative … append.
 #L1 #L2 #L3 elim L3 -L3 //
 qed.
 
-lemma append_shift: ∀L,K,I. L@@(ⓘ{I}.K) = (L.ⓘ{I})@@K.
+lemma append_shift: ∀L,K,I. L+(ⓘ{I}.K) = (L.ⓘ{I})+K.
 #L #K #I <append_assoc //
 qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma append_inv_atom3_sn: ∀L,K. ⋆ = L @@ K → ∧∧ ⋆ = L & ⋆ = K.
+lemma append_inv_atom3_sn: ∀L,K. ⋆ = L + K → ∧∧ ⋆ = L & ⋆ = K.
 #L * /2 width=1 by conj/
 #K #I >append_bind #H destruct
 qed-.
 
-lemma append_inv_bind3_sn: ∀I0,L,L0,K. L0.ⓘ{I0} = L @@ K →
+lemma append_inv_bind3_sn: ∀I0,L,L0,K. L0.ⓘ{I0} = L + K →
                            ∨∨ ∧∧ L0.ⓘ{I0} = L & ⋆ = K
-                            | ∃∃K0. K = K0.ⓘ{I0} & L0 = L @@ K0.
+                            | ∃∃K0. K = K0.ⓘ{I0} & L0 = L + K0.
 #I0 #L #L0 * /3 width=1 by or_introl, conj/
 #K #I >append_bind #H destruct /3 width=3 by ex2_intro, or_intror/
 qed-.
 
-lemma append_inj_sn: ∀K,L1,L2. L1@@K = L2@@K → L1 = L2.
+lemma append_inj_sn: ∀K,L1,L2. L1+K = L2+K → L1 = L2.
 #K elim K -K //
 #K #I #IH #L1 #L2 >append_bind #H
 elim (destruct_lbind_lbind_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma
index 9291ba5d1..c1133e8c0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma
@@ -19,7 +19,7 @@ include "basic_2/syntax/append.ma".
 
 (* Properties with length for local environments ****************************)
 
-lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|.
+lemma append_length: ∀L1,L2. |L1 + L2| = |L1| + |L2|.
 #L1 #L2 elim L2 -L2 //
 #L2 #I >append_bind >length_bind >length_bind //
 qed.
@@ -49,7 +49,7 @@ qed-.
 (* Inversion lemmas with length for local environments **********************)
 
 (* Basic_2A1: was: append_inj_sn *)
-lemma append_inj_length_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| →
+lemma append_inj_length_sn: ∀K1,K2,L1,L2. L1 + K1 = L2 + K2 → |K1| = |K2| →
                             L1 = L2 ∧ K1 = K2.
 #K1 elim K1 -K1
 [ * /2 width=1 by conj/
@@ -67,7 +67,7 @@ qed-.
 
 (* Note: lemma 750 *)
 (* Basic_2A1: was: append_inj_dx *)
-lemma append_inj_length_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| →
+lemma append_inj_length_dx: ∀K1,K2,L1,L2. L1 + K1 = L2 + K2 → |L1| = |L2| →
                             L1 = L2 ∧ K1 = K2.
 #K1 elim K1 -K1
 [ * /2 width=1 by conj/
@@ -87,15 +87,15 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma append_inj_dx: ∀L,K1,K2. L@@K1 = L@@K2 → K1 = K2.
+lemma append_inj_dx: ∀L,K1,K2. L+K1 = L+K2 → K1 = K2.
 #L #K1 #K2 #H elim (append_inj_length_dx … H) -H //
 qed-.
 
-lemma append_inv_refl_dx: ∀L,K. L@@K = L → K = ⋆.
+lemma append_inv_refl_dx: ∀L,K. L+K = L → K = ⋆.
 #L #K #H elim (append_inj_dx … (⋆) … H) //
 qed-.
 
-lemma append_inv_pair_dx: ∀I,L,K,V. L@@K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
+lemma append_inv_pair_dx: ∀I,L,K,V. L+K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
 #I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma
index 1de2ef352..cbb43ebb2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma
@@ -32,7 +32,7 @@ interpretation "application to vector (term)"
 lemma applv_nil: ∀T. Ⓐ◊.T = T.
 // qed.
 
-lemma applv_cons: ∀V,Vs,T. ⒶV@Vs.T = ⓐV.ⒶVs.T.
+lemma applv_cons: ∀V,Vs,T. ⒶV⨮Vs.T = ⓐV.ⒶVs.T.
 // qed.
 
 (* Properties with simple terms *********************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/list2_append.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/list2_append.etc
new file mode 100644
index 000000000..cf3b46445
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/list2_append.etc
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/oplus_4.ma".
+include "ground_2/lib/list2.ma".
+
+(* LISTS OF PAIRS ***********************************************************)
+
+rec definition append2 A1 A2 (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
+[ nil2           ⇒ l2
+| cons2 a1 a2 tl ⇒ {a1, a2} ⨮ append2 A1 A2 tl l2
+].
+
+interpretation "append (list of pairs)"
+   'OPlus A1 A2 l1 l2 = (append2 A1 A2 l1 l2).
diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/append_2.ma b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/oplus_4.etc
similarity index 73%
rename from matita/matita/contribs/lambdadelta/ground_2/notation/functions/append_2.ma
rename to matita/matita/contribs/lambdadelta/ground_2/etc/lib/oplus_4.etc
index f6d95184b..7905d518f 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/append_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/oplus_4.etc
@@ -14,6 +14,16 @@
 
 (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
 
-notation "hvbox( l1 @@ break l2 )"
-  right associative with precedence 47
-  for @{ 'Append $l1 $l2 }.
+notation < "hvbox( l1 ⊕ break l2 )"
+  left associative with precedence 60
+  for @{ 'OPlus $A $B $l1 $l2 }.
+
+notation > "hvbox( l1 ⊕ break l2 )"
+  left associative with precedence 60
+  for @{ 'OPlus ? ? $l1 $l2 }.
+(*
+(**) fix pair notation
+notation > "hvbox( l1 ⊕{ break term 46 A, break term 46 A } break term 61 l2 )"
+  non associative with precedence 60
+  for @{ 'OPlus $A $B $l1 $l2 }.
+*)
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
index 3ec2d22c7..ffce31286 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/notation/constructors/nil_0.ma".
-include "ground_2/notation/constructors/cons_2.ma".
+include "ground_2/notation/constructors/oplusright_3.ma".
 include "ground_2/lib/arith.ma".
 
 (* LISTS ********************************************************************)
@@ -24,9 +24,9 @@ inductive list (A:Type[0]) : Type[0] :=
 
 interpretation "nil (list)" 'Nil = (nil ?).
 
-interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
+interpretation "cons (list)" 'OPlusRight A hd tl = (cons A hd tl).
 
-rec definition length (A:Type[0]) (l:list A) on l ≝ match l with
+rec definition length A (l:list A) on l ≝ match l with
 [ nil      ⇒ 0
 | cons _ l ⇒ ↑(length A l)
 ].
@@ -45,7 +45,7 @@ rec definition all A (R:predicate A) (l:list A) on l ≝
 lemma length_nil (A:Type[0]): |nil A| = 0.
 // qed.
 
-lemma length_cons (A:Type[0]) (l:list A) (a:A): |a@l| = ↑|l|.
+lemma length_cons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|.
 // qed.
 
 (* Basic inversion lemmas on length *****************************************)
@@ -58,11 +58,11 @@ lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| → l = ◊.
 /2 width=1 by length_inv_zero_dx/ qed-.
 
 lemma length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ↑x →
-                         ∃∃tl,a. x = |tl| & l = a @ tl.
+                         ∃∃tl,a. x = |tl| & l = a ⨮ tl.
 #A * /2 width=4 by ex2_2_intro/
 >length_nil #x #H destruct
 qed-.
 
 lemma length_inv_succ_sn (A:Type[0]) (l:list A) (x): ↑x = |l| →
-                         ∃∃tl,a. x = |tl| & l = a @ tl.
+                         ∃∃tl,a. x = |tl| & l = a ⨮ tl.
 /2 width=1 by length_inv_succ_dx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma
index 68f2d0628..f9d93b74e 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma
@@ -13,8 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/notation/constructors/nil_0.ma".
-include "ground_2/notation/constructors/cons_3.ma".
-include "ground_2/notation/functions/append_2.ma".
+include "ground_2/notation/constructors/oplusright_5.ma".
 include "ground_2/lib/arith.ma".
 
 (* LISTS OF PAIRS ***********************************************************)
@@ -25,17 +24,10 @@ inductive list2 (A1,A2:Type[0]) : Type[0] :=
 
 interpretation "nil (list of pairs)" 'Nil = (nil2 ? ?).
 
-interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).
+interpretation "cons (list of pairs)"
+  'OPlusRight A1 A2 hd1 hd2 tl = (cons2 A1 A2 hd1 hd2 tl).
 
-rec definition append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
-[ nil2           ⇒ l2
-| cons2 a1 a2 tl ⇒ {a1, a2} @ append2 A1 A2 tl l2
-].
-
-interpretation "append (list of pairs)"
-   'Append l1 l2 = (append2 ? ? l1 l2).
-
-rec definition length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with
+rec definition length2 A1 A2 (l:list2 A1 A2) on l ≝ match l with
 [ nil2        ⇒ 0
 | cons2 _ _ l ⇒ ↑(length2 A1 A2 l)
 ].
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma
index 4ae6c939a..a308e5481 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/constructors/cons_2.ma".
+include "ground_2/notation/constructors/oplusright_3.ma".
 include "ground_2/lib/relations.ma".
 
 (* STREAMS ******************************************************************)
@@ -21,10 +21,10 @@ coinductive stream (A:Type[0]): Type[0] ≝
 | seq: A → stream A → stream A
 .
 
-interpretation "cons (nstream)" 'Cons b t = (seq ? b t).
+interpretation "cons (nstream)" 'OPlusRight A a u = (seq A a u).
 
 (* Basic properties *********************************************************)
 
-lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a @ u ] = t.
+lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a ⨮ u ] = t.
 #A * //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma
index a9940337e..878185ca1 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma
@@ -18,7 +18,7 @@ include "ground_2/lib/streams.ma".
 (* STREAMS ******************************************************************)
 
 coinductive eq_stream (A): relation (stream A) ≝
-| eq_seq: ∀t1,t2,b1,b2. b1 = b2 → eq_stream A t1 t2 → eq_stream A (b1@t1) (b2@t2)
+| eq_seq: ∀t1,t2,b1,b2. b1 = b2 → eq_stream A t1 t2 → eq_stream A (b1⨮t1) (b2⨮t2)
 .
 
 interpretation "extensional equivalence (nstream)"
@@ -36,7 +36,7 @@ definition eq_stream_repl_fwd (A) (R:predicate …) ≝
 (* Basic inversion lemmas ***************************************************)
 
 lemma eq_stream_inv_seq: ∀A,t1,t2. t1 ≗{A} t2 →
-                         ∀u1,u2,a1,a2. a1@u1 = t1 → a2@u2 = t2 →
+                         ∀u1,u2,a1,a2. a1⨮u1 = t1 → a2⨮u2 = t2 →
                          u1 ≗ u2 ∧ a1 = a2.
 #A #t1 #t2 * -t1 -t2
 #t1 #t2 #b1 #b2 #Hb #Ht #u1 #u2 #a1 #a2 #H1 #H2 destruct /2 width=1 by conj/
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
index c85459664..f128e5f73 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/functions/downspoon_1.ma".
+include "ground_2/notation/functions/downspoon_2.ma".
 include "ground_2/lib/streams_eq.ma".
 include "ground_2/lib/arith.ma".
 
@@ -24,16 +24,16 @@ definition hd (A:Type[0]): stream A → A ≝
 definition tl (A:Type[0]): stream A → stream A ≝
               λt. match t with [ seq _ t ⇒ t ].
 
-interpretation "tail (streams)" 'DownSpoon t = (tl ? t).
+interpretation "tail (streams)" 'DownSpoon A t = (tl A t).
 
 (* basic properties *********************************************************)
 
-lemma hd_rew (A) (a) (t): a = hd A (a@t).
+lemma hd_rew (A) (a) (t): a = hd A (a⨮t).
 // qed.
 
-lemma tl_rew (A) (a) (t): t = tl A (a@t).
+lemma tl_rew (A) (a) (t): t = tl A (a⨮t).
 // qed.
 
-lemma eq_stream_split (A) (t): (hd … t) @ ⫰t ≗{A} t.
+lemma eq_stream_split (A) (t): (hd … t) ⨮ ⫰t ≗{A} t.
 #A * //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma
index 13bdf51a2..f2a910aa0 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/functions/downspoonstar_2.ma".
+include "ground_2/notation/functions/downspoonstar_3.ma".
 include "ground_2/lib/streams_hdtl.ma".
 
 (* STREAMS ******************************************************************)
@@ -21,7 +21,7 @@ rec definition tls (A:Type[0]) (n:nat) on n: stream A → stream A ≝ ?.
 cases n -n [ #t @t | #n #t @tl @(tls … n t) ]
 defined.
 
-interpretation "recursive tail (strams)" 'DownSpoonStar n f = (tls ? n f).
+interpretation "iterated tail (strams)" 'DownSpoonStar A n f = (tls A n f).
 
 (* basic properties *********************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma
index 6da02adc1..8ea93cad8 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma
@@ -16,14 +16,14 @@
 
 notation < "hvbox( { term 46 hd1, break term 46 hd2 }⨮ break term 46 tl )"
   non associative with precedence 47
-  for @{ 'OplusRight $S1 $S2 $hd1 $hd2 $tl }.
+  for @{ 'OPlusRight $S1 $S2 $hd1 $hd2 $tl }.
 
 notation > "hvbox( { term 46 hd1, break term 46 hd2 }⨮ break term 46 tl )"
   non associative with precedence 47
-  for @{ 'OplusRight ? ? $hd1 $hd2 $tl }.
+  for @{ 'OPlusRight ? ? $hd1 $hd2 $tl }.
 (*
 (**) fix pair notation
 notation > "hvbox( { term 46 hd1, break term 46 hd2 }⨮{ break term 46 S1, break term 46 S2 } break term 46 tl )"
   non associative with precedence 47
-  for @{ 'OplusRight $S1 $S2 $hd1 $hd2 $tl }.
+  for @{ 'OPlusRight $S1 $S2 $hd1 $hd2 $tl }.
 *)
diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoon_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoon_2.ma
similarity index 79%
rename from matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoon_1.ma
rename to matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoon_2.ma
index c342d80b9..3b7824afc 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoon_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoon_2.ma
@@ -14,6 +14,14 @@
 
 (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
 
-notation "hvbox( â«° term 46 T )"
+notation < "hvbox( â«° term 46 a )"
    non associative with precedence 46
-   for @{ 'DownSpoon $T }.
+   for @{ 'DownSpoon $S $a }.
+
+notation > "hvbox( â«° term 46 a )"
+   non associative with precedence 46
+   for @{ 'DownSpoon ? $a }.
+
+notation > "hvbox( â«°{ term 46 S } break term 46 a )"
+   non associative with precedence 46
+   for @{ 'DownSpoon $S $a }.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoonstar_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoonstar_3.ma
similarity index 74%
rename from matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoonstar_2.ma
rename to matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoonstar_3.ma
index da7698c43..c6ad562a3 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoonstar_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/downspoonstar_3.ma
@@ -14,6 +14,14 @@
 
 (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
 
-notation "hvbox( â«° * [ term 46 n ] term 46 T )"
+notation < "hvbox( â«°*[ break term 46 n ] break term 46 a )"
    non associative with precedence 46
-   for @{ 'DownSpoonStar $n $T }.
+   for @{ 'DownSpoonStar $S $n $a }.
+
+notation > "hvbox( â«°*[ break term 46 n ] break term 46 a )"
+   non associative with precedence 46
+   for @{ 'DownSpoonStar ? $n $a }.
+
+notation > "hvbox( â«°*{ term 46 S }[ break term 46 n ] break term 46 a )"
+   non associative with precedence 46
+   for @{ 'DownSpoonStar $S $n $a }.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma
index a374857d4..2e148b71d 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma
@@ -20,9 +20,9 @@ include "ground_2/relocation/mr2.ma".
 inductive at: mr2 → relation nat ≝
 | at_nil: ∀i. at (◊) i i
 | at_lt : ∀cs,l,m,i1,i2. i1 < l →
-          at cs i1 i2 → at ({l, m} @ cs) i1 i2
+          at cs i1 i2 → at ({l, m} ⨮ cs) i1 i2
 | at_ge : ∀cs,l,m,i1,i2. l ≤ i1 →
-          at cs (i1 + m) i2 → at ({l, m} @ cs) i1 i2
+          at cs (i1 + m) i2 → at ({l, m} ⨮ cs) i1 i2
 .
 
 interpretation "application (multiple relocation with pairs)"
@@ -42,7 +42,7 @@ lemma at_inv_nil: ∀i1,i2. @⦃i1, ◊⦄ ≘ i2 → i1 = i2.
 /2 width=3 by at_inv_nil_aux/ qed-.
 
 fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≘ i2 →
-                      ∀l,m,cs0. cs = {l, m} @ cs0 →
+                      ∀l,m,cs0. cs = {l, m} ⨮ cs0 →
                       i1 < l ∧ @⦃i1, cs0⦄ ≘ i2 ∨
                       l ≤ i1 ∧ @⦃i1 + m, cs0⦄ ≘ i2.
 #cs #i1 #i2 * -cs -i1 -i2
@@ -52,19 +52,19 @@ fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≘ i2 →
 ]
 qed-.
 
-lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≘ i2 →
+lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m} ⨮ cs⦄ ≘ i2 →
                    i1 < l ∧ @⦃i1, cs⦄ ≘ i2 ∨
                    l ≤ i1 ∧ @⦃i1 + m, cs⦄ ≘ i2.
 /2 width=3 by at_inv_cons_aux/ qed-.
 
-lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≘ i2 →
+lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} ⨮ cs⦄ ≘ i2 →
                       i1 < l → @⦃i1, cs⦄ ≘ i2.
 #cs #l #m #i1 #m2 #H
 elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l
 elim (lt_le_false … Hi1l Hli1)
 qed-.
 
-lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≘ i2 →
+lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} ⨮ cs⦄ ≘ i2 →
                       l ≤ i1 → @⦃i1 + m, cs⦄ ≘ i2.
 #cs #l #m #i1 #m2 #H
 elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma
index b68e54959..b721754b6 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma
@@ -20,9 +20,9 @@ include "ground_2/relocation/mr2.ma".
 inductive minuss: nat → relation mr2 ≝
 | minuss_nil: ∀i. minuss i (◊) (◊)
 | minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 →
-              minuss i ({l, m} @ cs1) ({l - i, m} @ cs2)
+              minuss i ({l, m} ⨮ cs1) ({l - i, m} ⨮ cs2)
 | minuss_ge : ∀cs1,cs2,l,m,i. l ≤ i → minuss (m + i) cs1 cs2 →
-              minuss i ({l, m} @ cs1) cs2
+              minuss i ({l, m} ⨮ cs1) cs2
 .
 
 interpretation "minus (multiple relocation with pairs)"
@@ -42,10 +42,10 @@ lemma minuss_inv_nil1: ∀cs2,i. ◊ ▭ i ≘ cs2 → cs2 = ◊.
 /2 width=4 by minuss_inv_nil1_aux/ qed-.
 
 fact minuss_inv_cons1_aux: ∀cs1,cs2,i. cs1 ▭ i ≘ cs2 →
-                           ∀l,m,cs. cs1 = {l, m} @ cs →
+                           ∀l,m,cs. cs1 = {l, m} ⨮ cs →
                            l ≤ i ∧ cs ▭ m + i ≘ cs2 ∨
                            ∃∃cs0. i < l & cs ▭ i ≘ cs0 &
-                                   cs2 = {l - i, m} @ cs0.
+                                   cs2 = {l - i, m} ⨮ cs0.
 #cs1 #cs2 #i * -cs1 -cs2 -i
 [ #i #l #m #cs #H destruct
 | #cs1 #cs #l1 #m1 #i1 #Hil1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=3 by ex3_intro, or_intror/
@@ -53,22 +53,22 @@ fact minuss_inv_cons1_aux: ∀cs1,cs2,i. cs1 ▭ i ≘ cs2 →
 ]
 qed-.
 
-lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≘ cs2 →
+lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m} ⨮ cs1 ▭ i ≘ cs2 →
                         l ≤ i ∧ cs1 ▭ m + i ≘ cs2 ∨
                         ∃∃cs. i < l & cs1 ▭ i ≘ cs &
-                               cs2 = {l - i, m} @ cs.
+                               cs2 = {l - i, m} ⨮ cs.
 /2 width=3 by minuss_inv_cons1_aux/ qed-.
 
-lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≘ cs2 →
+lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} ⨮ cs1 ▭ i ≘ cs2 →
                            l ≤ i → cs1 ▭ m + i ≘ cs2.
 #cs1 #cs2 #l #m #i #H
 elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli
 elim (lt_le_false … Hil Hli)
 qed-.
 
-lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≘ cs2 →
+lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} ⨮ cs1 ▭ i ≘ cs2 →
                            i < l →
-                           ∃∃cs. cs1 ▭ i ≘ cs & cs2 = {l - i, m} @ cs.
+                           ∃∃cs. cs1 ▭ i ≘ cs & cs2 = {l - i, m} ⨮ cs.
 #cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
 #Hli #_ #Hil elim (lt_le_false … Hil Hli)
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma
index 8c3221597..7d9e5e603 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma
@@ -18,7 +18,7 @@ include "ground_2/relocation/mr2.ma".
 
 rec definition pluss (cs:mr2) (i:nat) on cs ≝ match cs with
 [ nil2         ⇒ ◊
-| cons2 l m cs ⇒ {l + i, m} @ pluss cs i
+| cons2 l m cs ⇒ {l + i, m} ⨮ pluss cs i
 ].
 
 interpretation "plus (multiple relocation with pairs)"
@@ -26,7 +26,7 @@ interpretation "plus (multiple relocation with pairs)"
 
 (* Basic properties *********************************************************)
 
-lemma pluss_SO2: ∀l,m,cs. ({l, m} @ cs) + 1 = {↑l, m} @ cs + 1.
+lemma pluss_SO2: ∀l,m,cs. ({l, m} ⨮ cs) + 1 = {↑l, m} ⨮ cs + 1.
 normalize // qed.
 
 (* Basic inversion lemmas ***************************************************)
@@ -36,8 +36,8 @@ lemma pluss_inv_nil2: ∀i,cs. cs + i = ◊ → cs = ◊.
 #l #m #cs #H destruct
 qed.
 
-lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} @ cs2 →
-                       ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} @ cs1.
+lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} ⨮ cs2 →
+                       ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} ⨮ cs1.
 #i #l #m #cs2 *
 [ normalize #H destruct
 | #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
index 2106418bc..3803c254b 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
@@ -19,22 +19,22 @@ include "ground_2/lib/streams_tls.ma".
 
 definition rtmap: Type[0] ≝ stream nat.
 
-definition push: rtmap → rtmap ≝ λf. 0@f.
+definition push: rtmap → rtmap ≝ λf. 0⨮f.
 
 interpretation "push (nstream)" 'UpSpoon f = (push f).
 
 definition next: rtmap → rtmap.
-* #n #f @(↑n@f)
+* #n #f @(↑n⨮f)
 defined.
 
 interpretation "next (nstream)" 'UpArrow f = (next f).
 
 (* Basic properties *********************************************************)
 
-lemma push_rew: ∀f. 0@f = ⫯f.
+lemma push_rew: ∀f. 0⨮f = ⫯f.
 // qed.
 
-lemma next_rew: ∀f,n. (↑n)@f = ↑(n@f).
+lemma next_rew: ∀f,n. (↑n)⨮f = ↑(n⨮f).
 // qed.
 
 (* Basic inversion lemmas ***************************************************)
@@ -55,19 +55,19 @@ lemma injective_next: injective ? ? next.
 * #n1 #f1 * #n2 #f2 normalize #H destruct //
 qed-.
 
-lemma push_inv_seq_sn: ∀f,g,n. n@g = ⫯f → 0 = n ∧ g = f.
+lemma push_inv_seq_sn: ∀f,g,n. n⨮g = ⫯f → 0 = n ∧ g = f.
 #f #g #n <push_rew #H destruct /2 width=1 by conj/
 qed-.
 
-lemma push_inv_seq_dx: ∀f,g,n. ⫯f = n@g → 0 = n ∧ g = f.
+lemma push_inv_seq_dx: ∀f,g,n. ⫯f = n⨮g → 0 = n ∧ g = f.
 #f #g #n <push_rew #H destruct /2 width=1 by conj/
 qed-.
 
-lemma next_inv_seq_sn: ∀f,g,n. n@g = ↑f → ∃∃m. m@g = f & ↑m = n.
+lemma next_inv_seq_sn: ∀f,g,n. n⨮g = ↑f → ∃∃m. m⨮g = f & ↑m = n.
 * #m #f #g #n <next_rew #H destruct /2 width=3 by ex2_intro/
 qed-.
 
-lemma next_inv_seq_dx: ∀f,g,n. ↑f = n@g → ∃∃m. m@g = f & ↑m = n.
+lemma next_inv_seq_dx: ∀f,g,n. ↑f = n⨮g → ∃∃m. m⨮g = f & ↑m = n.
 * #m #f #g #n <next_rew #H destruct /2 width=3 by ex2_intro/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
index 4724aa8be..0f21ba6c3 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
@@ -27,8 +27,8 @@ interpretation "functional composition (nstream)"
 
 (* Basic properies on compose ***********************************************)
 
-lemma compose_rew: ∀f2,f1,n1. f2@❴n1❵@(⫰*[↑n1]f2)∘f1 = f2∘(n1@f1).
-#f2 #f1 #n1 <(stream_rew … (f2∘(n1@f1))) normalize //
+lemma compose_rew: ∀f2,f1,n1. f2@❴n1❵⨮(⫰*[↑n1]f2)∘f1 = f2∘(n1⨮f1).
+#f2 #f1 #n1 <(stream_rew … (f2∘(n1⨮f1))) normalize //
 qed.
 
 lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
@@ -38,26 +38,26 @@ qed.
 
 (* Basic inversion lemmas on compose ****************************************)
 
-lemma compose_inv_rew: ∀f2,f1,f,n1,n. f2∘(n1@f1) = n@f →
+lemma compose_inv_rew: ∀f2,f1,f,n1,n. f2∘(n1⨮f1) = n⨮f →
                        f2@❴n1❵ = n ∧ (⫰*[↑n1]f2)∘f1 = f.
-#f2 #f1 #f #n1 #n <(stream_rew … (f2∘(n1@f1))) normalize
+#f2 #f1 #f #n1 #n <(stream_rew … (f2∘(n1⨮f1))) normalize
 #H destruct /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_O2: ∀f2,f1,f,n2,n. (n2@f2)∘(⫯f1) = n@f →
+lemma compose_inv_O2: ∀f2,f1,f,n2,n. (n2⨮f2)∘(⫯f1) = n⨮f →
                       n2 = n ∧ f2∘f1 = f.
 #f2 #f1 #f #n2 #n <compose_rew
 #H destruct /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_S2: ∀f2,f1,f,n2,n1,n. (n2@f2)∘(↑n1@f1) = n@f →
-                      ↑(n2+f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
+lemma compose_inv_S2: ∀f2,f1,f,n2,n1,n. (n2⨮f2)∘(↑n1⨮f1) = n⨮f →
+                      ↑(n2+f2@❴n1❵) = n ∧ f2∘(n1⨮f1) = f2@❴n1❵⨮f.
 #f2 #f1 #f #n2 #n1 #n <compose_rew
 #H destruct <tls_S1 /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_S1: ∀f2,f1,f,n1,n. (↑f2)∘(n1@f1) = n@f →
-                      ↑(f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
+lemma compose_inv_S1: ∀f2,f1,f,n1,n. (↑f2)∘(n1⨮f1) = n⨮f →
+                      ↑(f2@❴n1❵) = n ∧ f2∘(n1⨮f1) = f2@❴n1❵⨮f.
 #f2 #f1 #f #n1 #n <compose_rew
 #H destruct <tls_S1 /2 width=1 by conj/
 qed-.
@@ -65,16 +65,16 @@ qed-.
 (* Specific properties on after *********************************************)
 
 lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
-                ∀n. n@f2 ⊚ ⫯f1 ≘ n@f.
+                ∀n. n⨮f2 ⊚ ⫯f1 ≘ n⨮f.
 #f2 #f1 #f #Hf #n elim n -n /2 width=7 by after_refl, after_next/
 qed.
 
-lemma after_S2: ∀f2,f1,f,n1,n. f2 ⊚ n1@f1 ≘ n@f →
-                ∀n2. n2@f2 ⊚ ↑n1@f1 ≘ ↑(n2+n)@f.
+lemma after_S2: ∀f2,f1,f,n1,n. f2 ⊚ n1⨮f1 ≘ n⨮f →
+                ∀n2. n2⨮f2 ⊚ ↑n1⨮f1 ≘ ↑(n2+n)⨮f.
 #f2 #f1 #f #n1 #n #Hf #n2 elim n2 -n2 /2 width=7 by after_next, after_push/
 qed.
 
-lemma after_apply: ∀n1,f2,f1,f. (⫰*[↑n1] f2) ⊚ f1 ≘ f → f2 ⊚ n1@f1 ≘ f2@❴n1❵@f.
+lemma after_apply: ∀n1,f2,f1,f. (⫰*[↑n1] f2) ⊚ f1 ≘ f → f2 ⊚ n1⨮f1 ≘ f2@❴n1❵⨮f.
 #n1 elim n1 -n1
 [ * /2 width=1 by after_O2/
 | #n1 #IH * /3 width=1 by after_S2/
@@ -96,7 +96,7 @@ theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
 
 (* Specific inversion lemmas on after ***************************************)
 
-lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≘ n@f → ∀f1. ⫯f1 = g2 →
+lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2⨮f2 ⊚ g2 ≘ n⨮f → ∀f1. ⫯f1 = g2 →
                      f2 ⊚ f1 ≘ f ∧ n2 = n.
 #f2 #g2 #f #n2 elim n2 -n2
 [ #n #Hf #f1 #H2 elim (after_inv_ppx … Hf … H2) -g2 [2,3: // ]
@@ -108,8 +108,8 @@ lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≘ n@f → ∀f1. ⫯f1 = g2
 ]
 qed-.
 
-lemma after_inv_xnx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≘ n@f → ∀f1. ↑f1 = g2 →
-                     ∃∃m. f2 ⊚ f1 ≘ m@f & ↑(n2+m) = n.
+lemma after_inv_xnx: ∀f2,g2,f,n2,n. n2⨮f2 ⊚ g2 ≘ n⨮f → ∀f1. ↑f1 = g2 →
+                     ∃∃m. f2 ⊚ f1 ≘ m⨮f & ↑(n2+m) = n.
 #f2 #g2 #f #n2 elim n2 -n2
 [ #n #Hf #f1 #H2 elim (after_inv_pnx … Hf … H2) -g2 [2,3: // ]
   #g #Hf #H elim (next_inv_seq_dx … H) -H
@@ -121,7 +121,7 @@ lemma after_inv_xnx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≘ n@f → ∀f1. ↑f1 = g2
 ]
 qed-.
 
-lemma after_inv_const: ∀f2,f1,f,n1,n. n@f2 ⊚ n1@f1 ≘ n@f → f2 ⊚ f1 ≘ f ∧ 0 = n1.
+lemma after_inv_const: ∀f2,f1,f,n1,n. n⨮f2 ⊚ n1⨮f1 ≘ n⨮f → f2 ⊚ f1 ≘ f ∧ 0 = n1.
 #f2 #f1 #f #n1 #n elim n -n
 [ #H elim (after_inv_pxp … H) -H [ |*: // ]
   #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
@@ -134,12 +134,12 @@ lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
 
 (* Specific forward lemmas on after *****************************************)
 
-lemma after_fwd_hd: ∀f2,f1,f,n1,n. f2 ⊚ n1@f1 ≘ n@f → f2@❴n1❵ = n.
+lemma after_fwd_hd: ∀f2,f1,f,n1,n. f2 ⊚ n1⨮f1 ≘ n⨮f → f2@❴n1❵ = n.
 #f2 #f1 #f #n1 #n #H lapply (after_fwd_at ? n1 0 … H) -H [1,2,3: // ]
 /3 width=2 by at_inv_O1, sym_eq/
 qed-.
 
-lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2@f2 ⊚ n1@f1 ≘ n@f →
+lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f →
                      (⫰*[n1]f2) ⊚ f1 ≘ f.
 #f #f1 #n1 elim n1 -n1
 [ #f2 #n2 #n #H elim (after_inv_xpx … H) -H //
@@ -148,6 +148,6 @@ lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2@f2 ⊚ n1@f1 ≘ n@f →
 ]
 qed-.
 
-lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2@f2 ⊚ n1@f1 ≘ n@f →
-                       (n2@f2)@❴n1❵ = n ∧ (⫰*[n1]f2) ⊚ f1 ≘ f.
+lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f →
+                       (n2⨮f2)@❴n1❵ = n ∧ (⫰*[n1]f2) ⊚ f1 ≘ f.
 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
index 66ba11b18..775800328 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
@@ -24,13 +24,13 @@ rec definition fun0 (n1:nat) on n1: rtmap → nat.
 defined.
 
 rec definition fun2 (n1:nat) on n1: rtmap → rtmap.
-* * [ | #n2 #f2 @(n2@f2) ]
+* * [ | #n2 #f2 @(n2⨮f2) ]
 #f2 cases n1 -n1 [ @f2 ]
 #n1 @(fun2 n1 f2)
 defined.
 
 rec definition fun1 (n1:nat) (f1:rtmap) on n1: rtmap → rtmap.
-* * [ | #n2 #f2 @(n1@f1) ]
+* * [ | #n2 #f2 @(n1⨮f1) ]
 #f2 cases n1 -n1 [ @f1 ]
 #n1 @(fun1 n1 f1 f2)
 defined.
@@ -53,35 +53,35 @@ lemma fun2_xn: ∀f2,n1. f2 = fun2 n1 (↑f2).
 * #n2 #f2 * //
 qed.
 
-lemma fun1_xxn: ∀f2,f1,n1. fun1 n1 f1 (↑f2) = n1@f1.
+lemma fun1_xxn: ∀f2,f1,n1. fun1 n1 f1 (↑f2) = n1⨮f1.
 * #n2 #f2 #f1 * //
 qed.
 
 (* Basic properies on cocompose *********************************************)
 
-lemma cocompose_rew: ∀f2,f1,n1. (fun0 n1 f2)@(fun2 n1 f2)~∘(fun1 n1 f1 f2) = f2 ~∘ (n1@f1).
-#f2 #f1 #n1 <(stream_rew … (f2~∘(n1@f1))) normalize //
+lemma cocompose_rew: ∀f2,f1,n1. (fun0 n1 f2)⨮(fun2 n1 f2)~∘(fun1 n1 f1 f2) = f2 ~∘ (n1⨮f1).
+#f2 #f1 #n1 <(stream_rew … (f2~∘(n1⨮f1))) normalize //
 qed.
 
 (* Basic inversion lemmas on compose ****************************************)
 
-lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x@f →
+lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x⨮f →
                          0 = x ∧ f2 ~∘ f1 = f.
 #f2 #f1 #f #x
 <cocompose_rew #H destruct
 normalize /2 width=1 by conj/
 qed-.
 
-lemma cocompose_inv_pnx: ∀f2,f1,f,n1,x. (⫯f2) ~∘ ((↑n1)@f1) = x@f →
-                         ∃∃n. ↑n = x & f2 ~∘ (n1@f1) = n@f.
+lemma cocompose_inv_pnx: ∀f2,f1,f,n1,x. (⫯f2) ~∘ (↑n1⨮f1) = x⨮f →
+                         ∃∃n. ↑n = x & f2 ~∘ (n1⨮f1) = n⨮f.
 #f2 #f1 #f #n1 #x
 <cocompose_rew #H destruct
 @(ex2_intro … (fun0 n1 f2)) // <cocompose_rew
 /3 width=1 by eq_f2/
 qed-.
 
-lemma cocompose_inv_nxx: ∀f2,f1,f,n1,x. (↑f2) ~∘ (n1@f1) = x@f →
-                         0 = x ∧ f2 ~∘ (n1@f1) = f.
+lemma cocompose_inv_nxx: ∀f2,f1,f,n1,x. (↑f2) ~∘ (n1⨮f1) = x⨮f →
+                         0 = x ∧ f2 ~∘ (n1⨮f1) = f.
 #f2 #f1 #f #n1 #x
 <cocompose_rew #H destruct
 /2 width=1 by conj/
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma
index f4dc571fd..48f3e0100 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma
@@ -18,7 +18,7 @@ include "ground_2/relocation/rtmap_eq.ma".
 
 (* Specific properties ******************************************************)
 
-fact eq_inv_seq_aux: ∀f1,f2,n1,n2. n1@f1 ≡ n2@f2 → n1 = n2 ∧ f1 ≡ f2.
+fact eq_inv_seq_aux: ∀f1,f2,n1,n2. n1⨮f1 ≡ n2⨮f2 → n1 = n2 ∧ f1 ≡ f2.
 #f1 #f2 #n1 #n2 @(nat_elim2 … n1 n2) -n1 -n2
 [ #n2 #H elim (eq_inv_px … H) -H [2,3: // ]
   #g1 #H1 #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
@@ -28,7 +28,7 @@ fact eq_inv_seq_aux: ∀f1,f2,n1,n2. n1@f1 ≡ n2@f2 → n1 = n2 ∧ f1 ≡ f2.
 ]
 qed-.
 
-lemma eq_inv_seq: ∀g1,g2. g1 ≡ g2 → ∀f1,f2,n1,n2. n1@f1 = g1 → n2@f2 = g2 →
+lemma eq_inv_seq: ∀g1,g2. g1 ≡ g2 → ∀f1,f2,n1,n2. n1⨮f1 = g1 → n2⨮f2 = g2 →
                   n1 = n2 ∧ f1 ≡ f2.
 /2 width=1 by eq_inv_seq_aux/ qed-.
 
@@ -51,5 +51,5 @@ corec lemma nstream_inv_eq: ∀f1,f2. f1 ≗ f2 → f1 ≡ f2.
 #n @eq_next /3 width=5 by eq_seq/
 qed.
 
-lemma eq_seq_id: ∀f1,f2. f1 ≡ f2 → ∀n. n@f1 ≡ n@f2.
+lemma eq_seq_id: ∀f1,f2. f1 ≡ f2 → ∀n. n⨮f1 ≡ n⨮f2.
 /4 width=1 by nstream_inv_eq, nstream_eq, eq_seq/ qed.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_isid.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_isid.ma
index 91487980d..4f3e415eb 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_isid.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_isid.ma
@@ -19,7 +19,7 @@ include "ground_2/relocation/rtmap_isid.ma".
 
 (* Specific inversion lemmas ************************************************)
 
-lemma isid_inv_seq: ∀f,n. 𝐈⦃n@f⦄ → 𝐈⦃f⦄ ∧ 0 = n.
+lemma isid_inv_seq: ∀f,n. 𝐈⦃n⨮f⦄ → 𝐈⦃f⦄ ∧ 0 = n.
 #f #n #H elim (isid_inv_gen … H) -H
 #g #Hg #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
index 8dbd7ce38..5ceef8a1b 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
@@ -31,11 +31,11 @@ interpretation "functional application (nstream)"
 
 (* Specific properties on at ************************************************)
 
-lemma at_O1: ∀i2,f. @⦃0, i2@f⦄ ≘ i2.
+lemma at_O1: ∀i2,f. @⦃0, i2⨮f⦄ ≘ i2.
 #i2 elim i2 -i2 /2 width=5 by at_refl, at_next/
 qed.
 
-lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≘ i2 → @⦃↑i1, n@f⦄ ≘ ↑(n+i2).
+lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≘ i2 → @⦃↑i1, n⨮f⦄ ≘ ↑(n+i2).
 #n elim n -n /3 width=7 by at_push, at_next/
 qed.
 
@@ -47,20 +47,20 @@ qed.
 lemma at_istot: ∀f. 𝐓⦃f⦄.
 /2 width=2 by ex_intro/ qed.
 
-lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≘ i → @⦃i1, (m+n)@f⦄ ≘ m+i.
+lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n⨮f⦄ ≘ i → @⦃i1, (m+n)⨮f⦄ ≘ m+i.
 #f #i1 #i #n #m #H elim m -m //
 #m <plus_S1 /2 width=5 by at_next/ (**) (* full auto fails *)
 qed.
 
 (* Specific inversion lemmas on at ******************************************)
 
-lemma at_inv_O1: ∀f,n,i2. @⦃0, n@f⦄ ≘ i2 → n = i2.
+lemma at_inv_O1: ∀f,n,i2. @⦃0, n⨮f⦄ ≘ i2 → n = i2.
 #f #n elim n -n /2 width=6 by at_inv_ppx/
 #n #IH #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
 #j2 #Hj * -i2 /3 width=1 by eq_f/
 qed-.
 
-lemma at_inv_S1: ∀f,n,j1,i2. @⦃↑j1, n@f⦄ ≘ i2 →
+lemma at_inv_S1: ∀f,n,j1,i2. @⦃↑j1, n⨮f⦄ ≘ i2 →
                  ∃∃j2. @⦃j1, f⦄ ≘ j2 & ↑(n+j2) = i2.
 #f #n elim n -n /2 width=5 by at_inv_npx/
 #n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
@@ -73,7 +73,7 @@ lemma at_inv_total: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 → f@❴i1❵ = i2.
 
 (* Spercific forward lemmas on at *******************************************)
 
-lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n@f⦄ ≘ i2 → i1 + n ≤ i2.
+lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n⨮f⦄ ≘ i2 → i1 + n ≤ i2.
 #f #n *
 [ #i2 #H <(at_inv_O1 … H) -i2 //
 | #i1 #i2 #H elim (at_inv_S1 … H) -H
@@ -81,7 +81,7 @@ lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n@f⦄ ≘ i2 → i1 + n ≤ i2.
 ]
 qed-.
 
-lemma at_fwd_id: ∀f,n,i. @⦃i, n@f⦄ ≘ i → 0 = n.
+lemma at_fwd_id: ∀f,n,i. @⦃i, n⨮f⦄ ≘ i → 0 = n.
 #f #n #i #H elim (at_fwd_id_ex … H) -H
 #g #H elim (push_inv_seq_dx … H) -H //
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
index a7da5c2d0..65846a1b5 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -52,8 +52,8 @@ table {
    class "yellow"
    [ { "extensions to the library" * } {
         [ { "" * } {
-             [ "stream ( ? @ ? )" "stream_eq ( ? ≗ ? )" "stream_hdtl ( ⫰? )" "stream_tls ( ⫰*[?]? )" * ]
-             [ "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ]
+             [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
+             [ "list ( ◊ ) ( ? ⨮{?} ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} ⨮{?,?} ? ) ( |?| )" * ]
              [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ]
              [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "star" "ltc" * ]
           }
diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt
index 1661bc1f1..54e9d27e5 100644
--- a/matita/matita/contribs/lambdadelta/partial.txt
+++ b/matita/matita/contribs/lambdadelta/partial.txt
@@ -8,3 +8,4 @@ basic_2/i_static
 basic_2/rt_transition
 basic_2/rt_conversion
 apps_2/examples/ex_cpr_omega.ma
+apps_2/models/
-- 
2.39.2