From 873fb39bdd21aa14877bf5d50db26e3a050c6d43 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Thu, 30 Dec 2021 13:24:12 +0100
Subject: [PATCH] update in ground, static_2 and apps_2

+ updated notation for extensional equality
---
 .../apps_2/functional/mf_vlift_exteq.ma       |  4 +--
 .../apps_2/functional/mf_vpush_exteq.ma       |  4 +--
 .../apps_2/functional/mf_vpush_vlift.ma       |  4 +--
 .../lambdadelta/apps_2/models/tm_vpush.ma     |  2 +-
 .../lambdadelta/ground/arith/nat_iter.ma      |  6 ++--
 .../lambdadelta/ground/arith/nat_plus.ma      |  2 +-
 .../lambdadelta/ground/arith/nat_succ_iter.ma |  2 +-
 .../lambdadelta/ground/arith/pnat_iter.ma     |  8 ++---
 .../contribs/lambdadelta/ground/lib/exteq.ma  | 14 ++++----
 .../relations/{doteq_4.ma => circled_eq_4.ma} | 12 +++----
 .../ground/notation/relations/doteq_2.ma      | 19 +++++++++++
 .../ground/notation/relations/epsilon_3.ma    |  2 --
 .../ground/relocation/pr_after_after.ma       |  4 +--
 .../ground/relocation/pr_after_after_ist.ma   |  2 +-
 .../ground/relocation/pr_after_isi.ma         |  4 +--
 .../ground/relocation/pr_after_ist_isi.ma     |  4 +--
 .../ground/relocation/pr_coafter_coafter.ma   |  4 +--
 .../relocation/pr_coafter_coafter_ist.ma      |  2 +-
 .../ground/relocation/pr_coafter_isi.ma       |  2 +-
 .../ground/relocation/pr_compose.ma           |  2 +-
 .../lambdadelta/ground/relocation/pr_eq.ma    | 10 +++---
 .../lambdadelta/ground/relocation/pr_id_eq.ma |  4 +--
 .../ground/relocation/pr_isd_eq.ma            |  6 ++--
 .../ground/relocation/pr_isi_eq.ma            |  6 ++--
 .../ground/relocation/pr_isi_id.ma            |  4 +--
 .../ground/relocation/pr_isi_uni.ma           |  4 +--
 .../ground/relocation/pr_ist_ist.ma           |  2 +-
 .../ground/relocation/pr_isu_uni.ma           |  2 +-
 .../ground/relocation/pr_nexts_eq.ma          |  6 ++--
 .../ground/relocation/pr_pat_eq.ma            |  4 +--
 .../ground/relocation/pr_pat_id.ma            |  2 +-
 .../ground/relocation/pr_pat_tls.ma           |  4 +--
 .../ground/relocation/pr_pushs_eq.ma          |  2 +-
 .../ground/relocation/pr_sle_eq.ma            |  2 +-
 .../ground/relocation/pr_sor_isi.ma           |  4 +--
 .../ground/relocation/pr_sor_sor.ma           |  2 +-
 .../lambdadelta/ground/relocation/pr_tl_eq.ma | 32 +++++++++----------
 .../ground/relocation/pr_tl_eq_eq.ma          |  4 +--
 .../ground/relocation/pr_tls_eq.ma            |  2 +-
 .../ground/relocation/pr_tls_nexts_eq.ma      |  8 ++---
 .../ground/relocation/pr_tls_pushs_eq.ma      |  8 ++---
 .../ground/relocation/pr_uni_eq.ma            | 12 +++----
 .../ground/relocation/tr_compose_etc.ma       |  2 +-
 .../lambdadelta/ground/relocation/tr_eq.ma    |  4 +--
 .../lambdadelta/ground/web/ground_src.tbl     |  4 +--
 .../notation/relations/ideq_2.ma              |  2 +-
 .../lambdadelta/static_2/syntax/teq.ma        |  2 +-
 matita/matita/predefined_virtuals.ml          |  2 +-
 48 files changed, 133 insertions(+), 116 deletions(-)
 rename matita/matita/contribs/lambdadelta/ground/notation/relations/{doteq_4.ma => circled_eq_4.ma} (82%)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_2.ma
 rename matita/matita/contribs/lambdadelta/{ground => static_2}/notation/relations/ideq_2.ma (93%)

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma
index d7d6211ec..2e0249286 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma
@@ -20,7 +20,7 @@ include "apps_2/functional/mf_vlift.ma".
 
 (* Properties with extensional equivalence **********************************)
 
-lemma mf_gc_id: ∀j. ⇡[j]mf_gi ≐ mf_gi.
+lemma mf_gc_id: ∀j. ⇡[j]mf_gi ⊜ mf_gi.
 // qed.
 
 lemma mf_vlift_comp (l): compatible_2 … (mf_vlift l) (exteq …) (exteq …).
@@ -30,5 +30,5 @@ qed.
 
 (* Main properties with extensional equivalence *****************************)
 
-theorem mf_vlift_swap: ∀l1,l2. l2 ≤ l1 → ∀v. ⇡[l2]⇡[l1]v ≐ ⇡[↑l1]⇡[l2]v.
+theorem mf_vlift_swap: ∀l1,l2. l2 ≤ l1 → ∀v. ⇡[l2]⇡[l1]v ⊜ ⇡[↑l1]⇡[l2]v.
 /2 width=1 by flifts_basic_swap/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma
index 855934ca2..ccc1c34f0 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma
@@ -20,7 +20,7 @@ include "apps_2/functional/mf_vpush.ma".
 
 (* Properties with extensional equivalence **********************************)
 
-lemma mf_lc_id: ⇡[0←#0]mf_li ≐ mf_li.
+lemma mf_lc_id: ⇡[0←#0]mf_li ⊜ mf_li.
 #i elim (eq_or_gt i) #Hi destruct //
 >mf_vpush_gt // >(flifts_lref_uni 1) <(S_pred … Hi) in ⊢ (???%); -Hi //
 qed.
@@ -37,7 +37,7 @@ qed-.
 (* Main properties with extensional equivalence *****************************)
 
 theorem mf_vpush_swap: ∀l1,l2. l2 ≤ l1 →
-                       ∀v,T1,T2. ⇡[l2←T2]⇡[l1←T1]v ≐ ⇡[↑l1←↑[l2,1]T1]⇡[l2←T2]v.
+                       ∀v,T1,T2. ⇡[l2←T2]⇡[l1←T1]v ⊜ ⇡[↑l1←↑[l2,1]T1]⇡[l2←T2]v.
 #l1 #l2 #Hl21 #v #T1 #T2 #i
 elim (lt_or_eq_or_gt i l2) #Hl2 destruct
 [ lapply (lt_to_le_to_lt … Hl2 Hl21) #Hl1
diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma
index c1f6e76ce..1155e3487 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma
@@ -19,7 +19,7 @@ include "apps_2/functional/mf_vpush.ma".
 
 (* Properties with multiple filling lift ************************************)
 
-lemma mf_vpush_vlift_swap_O (v) (T) (l): ⇡[0←↑[↑l,1]T]⇡[l]v ≐⇡[↑l]⇡[0←T]v.
+lemma mf_vpush_vlift_swap_O (v) (T) (l): ⇡[0←↑[↑l,1]T]⇡[l]v ⊜⇡[↑l]⇡[0←T]v.
 #v #T #l #i
 elim (eq_or_gt i) #Hi destruct
 [ >mf_vpush_eq >mf_vlift_rw >mf_vpush_eq //
@@ -28,6 +28,6 @@ elim (eq_or_gt i) #Hi destruct
 ]
 qed.
 
-lemma mf_vpush_vlift_swap_O_lref_O (v) (l): ⇡[0←#0]⇡[l]v ≐⇡[↑l]⇡[0←#0]v.
+lemma mf_vpush_vlift_swap_O_lref_O (v) (l): ⇡[0←#0]⇡[l]v ⊜⇡[↑l]⇡[0←#0]v.
 #v #l @(mf_vpush_vlift_swap_O … (#0))
 qed.
diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma
index 1eae07864..d0460b09c 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma
@@ -19,7 +19,7 @@ include "apps_2/models/tm.ma".
 
 (* Properties with push for model evaluation ********************************)
 
-lemma tm_vpush_vlift_join_O (h) (v) (T): ⇡[0]⫯{TM h}[0←T]v ≐ ⇡[0←↑[1]T]v.
+lemma tm_vpush_vlift_join_O (h) (v) (T): ⇡[0]⫯{TM h}[0←T]v ⊜ ⇡[0←↑[1]T]v.
 #h #v #T #i
 elim (eq_or_gt i) #Hi destruct
 [ >mf_vpush_eq >mf_vlift_rw >vpush_eq //
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
index 6adaa148a..fc824317a 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
@@ -35,20 +35,20 @@ interpretation
 lemma niter_zero (A) (f) (a): a = (f^{A}𝟎) a.
 // qed.
 
-lemma niter_inj (A) (f) (p): f^p ≐ f^{A}(ninj p).
+lemma niter_inj (A) (f) (p): f^p ⊜ f^{A}(ninj p).
 // qed.
 
 (* Advanced constructions ***************************************************)
 
 (*** iter_n_Sm *)
-lemma niter_appl (A) (f) (n): f ∘ f^n ≐ f^{A}n ∘ f.
+lemma niter_appl (A) (f) (n): f ∘ f^n ⊜ f^{A}n ∘ f.
 #A #f * //
 #p @exteq_repl
 /2 width=5 by piter_appl, compose_repl_fwd_dx/
 qed.
 
 lemma niter_compose (A) (B) (f) (g) (h) (n):
-      h ∘ f ≐ g ∘ h → h ∘ (f^{A}n) ≐ (g^{B}n) ∘ h.
+      h ∘ f ⊜ g ∘ h → h ∘ (f^{A}n) ⊜ (g^{B}n) ∘ h.
 #A #B #f #g #h * //
 #p #H @exteq_repl
 /2 width=5 by piter_compose, compose_repl_fwd_dx/
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index a9894fc62..19b8acdd0 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -43,7 +43,7 @@ qed.
 
 (*** iter_plus *)
 lemma niter_plus (A) (f) (n1) (n2):
-      f^n2 ∘ f^n1 ≐ f^{A}(n1+n2).
+      f^n2 ∘ f^n1 ⊜ f^{A}(n1+n2).
 #A #f #n1 #n2 @(nat_ind_succ … n2) -n2 //
 #n2 #IH <nplus_succ_dx
 @exteq_repl
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma
index 7f47f9158..29e3e4d4f 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma
@@ -20,6 +20,6 @@ include "ground/arith/nat_succ.ma".
 (* Constructions with niter *************************************************)
 
 (*** iter_S *)
-lemma niter_succ (A) (f) (n): f ∘ f^n ≐ f^{A}(↑n).
+lemma niter_succ (A) (f) (n): f ∘ f^n ⊜ f^{A}(↑n).
 #A #f * //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
index 5361dcef3..95425f8eb 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
@@ -31,22 +31,22 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma piter_unit (A) (f): f ≐ f^{A}𝟏.
+lemma piter_unit (A) (f): f ⊜ f^{A}𝟏.
 // qed.
 
-lemma piter_succ (A) (f) (p): f ∘ f^p ≐ f^{A}(↑p).
+lemma piter_succ (A) (f) (p): f ∘ f^p ⊜ f^{A}(↑p).
 // qed.
 
 (* Advanced constructions ***************************************************)
 
-lemma piter_appl (A) (f) (p): f ∘ f^p ≐ f^{A}p ∘ f.
+lemma piter_appl (A) (f) (p): f ∘ f^p ⊜ f^{A}p ∘ f.
 #A #f #p elim p -p //
 #p #IH @exteq_repl
 /3 width=5 by compose_repl_fwd_dx, compose_repl_fwd_sn, exteq_canc_dx/
 qed.
 
 lemma piter_compose (A) (B) (f) (g) (h) (p):
-      h ∘ f ≐ g ∘ h → h ∘ (f^{A}p) ≐ (g^{B}p) ∘ h.
+      h ∘ f ⊜ g ∘ h → h ∘ (f^{A}p) ⊜ (g^{B}p) ∘ h.
 #A #B #f #g #h #p elim p -p
 [ #H @exteq_repl
   /2 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
index 81c5373a0..8c8f218a1 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/relations/doteq_4.ma".
+include "ground/notation/relations/circled_eq_4.ma".
 include "ground/lib/relations.ma".
 
 (* EXTENSIONAL EQUIVALENCE FOR FUNCTIONS ************************************)
@@ -22,7 +22,7 @@ definition exteq (A,B:Type[0]): relation (A → B) ≝
 
 interpretation
   "extensional equivalence"
-  'DotEq A B f1 f2 = (exteq A B f1 f2).
+  'CircledEq A B f1 f2 = (exteq A B f1 f2).
 
 (* Basic constructions ******************************************************)
 
@@ -53,27 +53,27 @@ lemma exteq_canc_dx (A) (B):
 (* Constructions with compose ***********************************************)
 
 lemma compose_repl_fwd_dx (A) (B) (C) (g) (f1) (f2):
-      f1 ≐{A,B} f2 → g ∘ f1 ≐{A,C} g ∘ f2.
+      f1 ⊜{A,B} f2 → g ∘ f1 ⊜{A,C} g ∘ f2.
 #A #B #C #g #f1 #f2 #Hf12 #a
 whd in ⊢ (??%%); //
 qed.
 
 lemma compose_repl_bak_dx (A) (B) (C) (g) (f1) (f2):
-      f1 ≐{A,B} f2 → g ∘ f2 ≐{A,C} g ∘ f1.
+      f1 ⊜{A,B} f2 → g ∘ f2 ⊜{A,C} g ∘ f1.
 /3 width=1 by compose_repl_fwd_dx, exteq_sym/
 qed.
 
 lemma compose_repl_fwd_sn (A) (B) (C) (g1) (g2) (f):
-      g1 ≐{B,C} g2 → g1 ∘ f ≐{A,C} g2 ∘ f.
+      g1 ⊜{B,C} g2 → g1 ∘ f ⊜{A,C} g2 ∘ f.
 #A #B #C #g1 #g2 #f #Hg12 #a
 whd in ⊢ (??%%); //
 qed.
 
 lemma compose_repl_bak_sn (A) (B) (C) (g1) (g2) (f):
-      g1 ≐{B,C} g2 → g2 ∘ f ≐{A,C} g1 ∘ f.
+      g1 ⊜{B,C} g2 → g2 ∘ f ⊜{A,C} g1 ∘ f.
 /3 width=1 by compose_repl_fwd_sn, exteq_sym/
 qed.
 
 lemma compose_assoc (A1) (A2) (A3) (A4) (f3:A3→A4) (f2:A2→A3) (f1:A1→A2):
-      f3 ∘ (f2 ∘ f1) ≐ f3 ∘ f2 ∘ f1.
+      f3 ∘ (f2 ∘ f1) ⊜ f3 ∘ f2 ∘ f1.
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/circled_eq_4.ma
similarity index 82%
rename from matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma
rename to matita/matita/contribs/lambdadelta/ground/notation/relations/circled_eq_4.ma
index 5ccb16c4b..4f602ce15 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/circled_eq_4.ma
@@ -14,14 +14,14 @@
 
 (* GROUND NOTATION **********************************************************)
 
-notation < "hvbox( term 46 f1 ≐ break term 46 f2 )"
+notation < "hvbox( f1 ⊜ break term 46 f2 )"
   non associative with precedence 45
-  for @{ 'DotEq $A $B $f1 $f2 }.
+  for @{ 'CircledEq $A $B $f1 $f2 }.
 
-notation > "hvbox( f1 ≐ break term 46 f2 )"
+notation > "hvbox( f1 ⊜ break term 46 f2 )"
   non associative with precedence 45
-  for @{ 'DotEq ? ? $f1 $f2 }.
+  for @{ 'CircledEq ? ? $f1 $f2 }.
 
-notation > "hvbox( f1 ≐{ break term 46 A, break term 46 B } break term 46 f2 )"
+notation > "hvbox( f1 ⊜{ break term 46 A, break term 46 B } break term 46 f2 )"
   non associative with precedence 45
-  for @{ 'DotEq $A $B $f1 $f2 }.
+  for @{ 'CircledEq $A $B $f1 $f2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_2.ma
new file mode 100644
index 000000000..46cfbb51b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_2.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( f1 ≐ break term 46 f2 )"
+  non associative with precedence 45
+  for @{ 'DotEq $f1 $f2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma
index 2f5287d6b..97639a36c 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
 (* GROUND NOTATION **********************************************************)
 
 notation < "hvbox( a ϵ break term 46 u )"
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma
index c048ec402..741da1062 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma
@@ -74,7 +74,7 @@ qed-.
 
 (*** after_mono *)
 corec theorem pr_after_mono:
-              ∀f1,f2,x,y. f1 ⊚ f2 ≘ x → f1 ⊚ f2 ≘ y → x ≡ y.
+              ∀f1,f2,x,y. f1 ⊚ f2 ≘ x → f1 ⊚ f2 ≘ y → x ≐ y.
 #f1 #f2 #x #y * -f1 -f2 -x
 #f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy
 [ cases (pr_after_inv_push_bi … Hy … H1 H2) -g1 -g2 /3 width=8 by pr_eq_push/
@@ -86,5 +86,5 @@ qed-.
 (*** after_mono_eq *)
 lemma pr_after_mono_eq:
       ∀f1,f2,f. f1 ⊚ f2 ≘ f → ∀g1,g2,g. g1 ⊚ g2 ≘ g →
-      f1 ≡ g1 → f2 ≡ g2 → f ≡ g.
+      f1 ≐ g1 → f2 ≐ g2 → f ≐ g.
 /4 width=4 by pr_after_mono, pr_after_eq_repl_back_dx, pr_after_eq_repl_back_sn/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma
index e67235f76..cb234dc2d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma
@@ -22,7 +22,7 @@ include "ground/relocation/pr_after_pat_tls.ma".
 (*** H_after_inj *)
 definition H_pr_after_inj: predicate pr_map ≝
            λf1. 𝐓❨f1❩ →
-           ∀f,f21,f22. f1 ⊚ f21 ≘ f → f1 ⊚ f22 ≘ f → f21 ≡ f22.
+           ∀f,f21,f22. f1 ⊚ f21 ≘ f → f1 ⊚ f22 ≘ f → f21 ≐ f22.
 
 (* Main destructions with pr_ist ********************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isi.ma
index 494659038..f5457f3c3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isi.ma
@@ -41,12 +41,12 @@ qed.
 
 (*** after_isid_inv_sn *)
 lemma pr_after_isi_inv_sn:
-      ∀f1,f2,f. f1 ⊚ f2 ≘ f → 𝐈❨f1❩ → f2 ≡ f.
+      ∀f1,f2,f. f1 ⊚ f2 ≘ f → 𝐈❨f1❩ → f2 ≐ f.
 /3 width=6 by pr_after_isi_sn, pr_after_mono/ qed-.
 
 (*** after_isid_inv_dx *)
 lemma pr_after_isi_inv_dx:
-      ∀f1,f2,f. f1 ⊚ f2 ≘ f → 𝐈❨f2❩ → f1 ≡ f.
+      ∀f1,f2,f. f1 ⊚ f2 ≘ f → 𝐈❨f2❩ → f1 ≐ f.
 /3 width=6 by pr_after_isi_dx, pr_after_mono/ qed-.
 
 (*** after_fwd_isid1 *)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
index 4e17044de..16d2ebc8d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_after_ist.ma".
 
 (*** after_fwd_isid_sn *)
 lemma pr_after_des_ist_eq_sn:
-      ∀f2,f1,f. 𝐓❨f❩ → f2 ⊚ f1 ≘ f → f1 ≡ f → 𝐈❨f2❩.
+      ∀f2,f1,f. 𝐓❨f❩ → f2 ⊚ f1 ≘ f → f1 ≐ f → 𝐈❨f2❩.
 #f2 #f1 #f #H #Hf elim (pr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H @pr_isi_pat_total // -Hf2
 #i2 #i #Hf2 elim (Hf1 i2) -Hf1
@@ -32,7 +32,7 @@ qed-.
 
 (*** after_fwd_isid_dx *)
 lemma pr_after_des_ist_eq_dx:
-      ∀f2,f1,f.  𝐓❨f❩ → f2 ⊚ f1 ≘ f → f2 ≡ f → 𝐈❨f1❩.
+      ∀f2,f1,f.  𝐓❨f❩ → f2 ⊚ f1 ≘ f → f2 ≐ f → 𝐈❨f1❩.
 #f2 #f1 #f #H #Hf elim (pr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H2 @pr_isi_pat_total // -Hf1
 #i1 #i2 #Hi12 elim (pr_after_des_ist_pat … Hi12 … Hf) -f1
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma
index 8ac9736a7..ff06a8c35 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma
@@ -20,7 +20,7 @@ include "ground/relocation/pr_coafter_eq.ma".
 
 (*** coafter_mono *)
 corec theorem pr_coafter_mono:
-              ∀f1,f2,x,y. f1 ~⊚ f2 ≘ x → f1 ~⊚ f2 ≘ y → x ≡ y.
+              ∀f1,f2,x,y. f1 ~⊚ f2 ≘ x → f1 ~⊚ f2 ≘ y → x ≐ y.
 #f1 #f2 #x #y * -f1 -f2 -x
 #f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy
 [ cases (pr_coafter_inv_push_bi … Hy … H1 H2) -g1 -g2 /3 width=8 by pr_eq_push/
@@ -32,5 +32,5 @@ qed-.
 (*** coafter_mono_eq *)
 lemma pr_coafter_mono_eq:
       ∀f1,f2,f. f1 ~⊚ f2 ≘ f → ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
-      f1 ≡ g1 → f2 ≡ g2 → f ≡ g.
+      f1 ≐ g1 → f2 ≐ g2 → f ≐ g.
 /4 width=4 by pr_coafter_mono, pr_coafter_eq_repl_back_dx, pr_coafter_eq_repl_back_sn/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
index d627e2597..e60d548e7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_coafter_nat_tls.ma".
 (*** H_coafter_inj *)
 definition H_pr_coafter_inj: predicate pr_map ≝
            λf1. 𝐓❨f1❩ →
-           ∀f,f21,f22. f1 ~⊚ f21 ≘ f → f1 ~⊚ f22 ≘ f → f21 ≡ f22.
+           ∀f,f21,f22. f1 ~⊚ f21 ≘ f → f1 ~⊚ f22 ≘ f → f21 ≐ f22.
 
 (* Main destructions with pr_ist ********************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma
index 7bed357e1..5ed452f2b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma
@@ -41,7 +41,7 @@ qed.
 
 (*** coafter_isid_inv_sn *)
 lemma pr_coafter_isi_inv_sn:
-      ∀f1,f2,f. f1 ~⊚ f2 ≘ f → 𝐈❨f1❩ → f2 ≡ f.
+      ∀f1,f2,f. f1 ~⊚ f2 ≘ f → 𝐈❨f1❩ → f2 ≐ f.
 /3 width=6 by pr_coafter_isi_sn, pr_coafter_mono/ qed-.
 
 (*** coafter_isid_inv_dx *)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
index 12ce1a69c..71a256c10 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
@@ -63,5 +63,5 @@ qed.
 (* Main inversions **********************************************************)
 
 (*** after_inv_total *)
-lemma pr_after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
+lemma pr_after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≐ f.
 /2 width=4 by pr_after_mono/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma
index 610ba9c7d..c908a6ac3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground/xoa/ex_3_2.ma".
-include "ground/notation/relations/ideq_2.ma".
+include "ground/notation/relations/doteq_2.ma".
 include "ground/lib/stream_eq.ma".
 include "ground/relocation/pr_map.ma".
 
@@ -31,19 +31,19 @@ coinductive pr_eq: relation pr_map ≝
 
 interpretation
   "extensional equivalence (partial relocation maps)"
-  'IdEq f1 f2 = (pr_eq f1 f2).
+  'DotEq f1 f2 = (pr_eq f1 f2).
 
 (*** eq_repl *)
 definition pr_eq_repl (R:relation …) ≝
-           ∀f1,f2. f1 ≡ f2 → R f1 f2.
+           ∀f1,f2. f1 ≐ f2 → R f1 f2.
 
 (*** eq_repl_back *)
 definition pr_eq_repl_back (R:predicate …) ≝
-           ∀f1. R f1 → ∀f2. f1 ≡ f2 → R f2.
+           ∀f1. R f1 → ∀f2. f1 ≐ f2 → R f2.
 
 (*** eq_repl_fwd *)
 definition pr_eq_repl_fwd (R:predicate …) ≝
-           ∀f1. R f1 → ∀f2. f2 ≡ f1 → R f2.
+           ∀f1. R f1 → ∀f2. f2 ≐ f1 → R f2.
 
 (* Basic constructions ******************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma
index 1e1fd6af5..cb7ff5bf5 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma
@@ -19,7 +19,7 @@ include "ground/relocation/pr_id.ma".
 
 (* Constructions with pr_eq *************************************************)
 
-corec lemma pr_id_eq (f): ⫯f ≡ f → 𝐢 ≡ f.
+corec lemma pr_id_eq (f): ⫯f ≐ f → 𝐢 ≐ f.
 cases pr_id_unfold #Hf
 cases (pr_eq_inv_push_sn … Hf) [|*: // ] #_ #H
 cases H in Hf; -H #Hf
@@ -30,7 +30,7 @@ qed.
 (* Inversions with pr_eq ****************************************************)
 
 (* Note: this has the same proof of the previous *)
-corec lemma pr_id_inv_eq (f): 𝐢 ≡ f → ⫯f ≡ f.
+corec lemma pr_id_inv_eq (f): 𝐢 ≐ f → ⫯f ≐ f.
 cases pr_id_unfold #Hf
 cases (pr_eq_inv_push_sn … Hf) [|*: // ] #_ #H
 cases H in Hf; -H #Hf
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_eq.ma
index a6000c810..9b00fda4d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_eq.ma
@@ -35,7 +35,7 @@ lemma pr_isd_eq_repl_fwd:
 (* Main inversions with pr_eq ***********************************************)
 
 (*** isdiv_inv_eq_repl *)
-corec theorem pr_isd_inv_eq_repl (g1) (g2): 𝛀❨g1❩ → 𝛀❨g2❩ → g1 ≡ g2.
+corec theorem pr_isd_inv_eq_repl (g1) (g2): 𝛀❨g1❩ → 𝛀❨g2❩ → g1 ≐ g2.
 #H1 #H2
 cases (pr_isd_inv_gen … H1) -H1
 cases (pr_isd_inv_gen … H2) -H2
@@ -45,13 +45,13 @@ qed-.
 (* Alternative definition with pr_eq ****************************************)
 
 (*** eq_next_isdiv *)
-corec lemma pr_eq_next_isd (f): ↑f ≡ f → 𝛀❨f❩.
+corec lemma pr_eq_next_isd (f): ↑f ≐ f → 𝛀❨f❩.
 #H cases (pr_eq_inv_next_sn … H) -H
 /4 width=3 by pr_isd_next, pr_eq_trans/
 qed.
 
 (*** eq_next_inv_isdiv *)
-corec lemma pr_eq_next_inv_isd (g): 𝛀❨g❩ → ↑g ≡ g.
+corec lemma pr_eq_next_inv_isd (g): 𝛀❨g❩ → ↑g ≐ g.
 * -g #f #g #Hf *
 /3 width=5 by pr_eq_next/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_eq.ma
index 58317065d..189567290 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_eq.ma
@@ -36,7 +36,7 @@ lemma pr_isi_eq_repl_fwd:
 (* Main inversions with pr_eq ***********************************************)
 
 (*** isid_inv_eq_repl *)
-corec theorem pr_isi_inv_eq_repl (g1) (g2): 𝐈❨g1❩ → 𝐈❨g2❩ → g1 ≡ g2.
+corec theorem pr_isi_inv_eq_repl (g1) (g2): 𝐈❨g1❩ → 𝐈❨g2❩ → g1 ≐ g2.
 #H1 #H2
 cases (pr_isi_inv_gen … H1) -H1
 cases (pr_isi_inv_gen … H2) -H2
@@ -46,13 +46,13 @@ qed-.
 (* Alternative definition with pr_eq ****************************************)
 
 (*** eq_push_isid *)
-corec lemma pr_eq_push_isi (f): ⫯f ≡ f → 𝐈❨f❩.
+corec lemma pr_eq_push_isi (f): ⫯f ≐ f → 𝐈❨f❩.
 #H cases (pr_eq_inv_push_sn … H) -H
 /4 width=3 by pr_isi_push, pr_eq_trans/
 qed.
 
 (*** eq_push_inv_isid *)
-corec lemma pr_isi_inv_eq_push (g): 𝐈❨g❩ → ⫯g ≡ g.
+corec lemma pr_isi_inv_eq_push (g): 𝐈❨g❩ → ⫯g ≐ g.
 * -g #f #g #Hf *
 /3 width=5 by pr_eq_push/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma
index 374fcdce4..9e3ffed09 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma
@@ -26,9 +26,9 @@ lemma pr_isi_id: 𝐈❨𝐢❩.
 (* Alternative definition with pr_id and pr_eq ******************************)
 
 (*** eq_id_isid *)
-lemma pr_eq_id_isi (f): 𝐢 ≡ f → 𝐈❨f❩.
+lemma pr_eq_id_isi (f): 𝐢 ≐ f → 𝐈❨f❩.
 /2 width=3 by pr_isi_eq_repl_back/ qed.
 
 (*** eq_id_inv_isid *)
-lemma pr_isi_inv_eq_id (f): 𝐈❨f❩ → 𝐢 ≡ f.
+lemma pr_isi_inv_eq_id (f): 𝐈❨f❩ → 𝐢 ≐ f.
 /2 width=1 by pr_isi_inv_eq_repl/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma
index 1db92adae..48c57a284 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma
@@ -20,11 +20,11 @@ include "ground/relocation/pr_isi_id.ma".
 (* Constructions with pr_isi ************************************************)
 
 (*** uni_inv_isid uni_isi *)
-lemma pr_uni_isi (f): 𝐮❨𝟎❩ ≡ f → 𝐈❨f❩.
+lemma pr_uni_isi (f): 𝐮❨𝟎❩ ≐ f → 𝐈❨f❩.
 /2 width=1 by pr_eq_id_isi/ qed.
 
 (* Inversions with pr_isi ***************************************************)
 
 (*** uni_isid isi_inv_uni *)
-lemma pr_isi_inv_uni (f): 𝐈❨f❩ → 𝐮❨𝟎❩ ≡ f.
+lemma pr_isi_inv_uni (f): 𝐈❨f❩ → 𝐮❨𝟎❩ ≐ f.
 /2 width=1 by pr_isi_inv_eq_id/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
index cfb786adc..de3ecfe4e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
@@ -47,7 +47,7 @@ qed-.
 (*** at_ext *)
 corec theorem pr_eq_ext_pat (f1) (f2): 𝐓❨f1❩ → 𝐓❨f2❩ →
               (∀i,i1,i2. @❨i,f1❩ ≘ i1 → @❨i,f2❩ ≘ i2 → i1 = i2) →
-              f1 ≡ f2.
+              f1 ≐ f2.
 cases (pr_map_split_tl f1) #H1
 cases (pr_map_split_tl f2) #H2
 #Hf1 #Hf2 #Hi
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
index 1e6706a8b..bb4cceede 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
@@ -43,7 +43,7 @@ lemma pr_isu_eq_repl_fwd:
 (* Inversions with pr_uni ***************************************************)
 
 (*** uni_isuni *)
-lemma pr_isu_inv_uni (f): 𝐔❨f❩ → ∃n. 𝐮❨n❩ ≡ f.
+lemma pr_isu_inv_uni (f): 𝐔❨f❩ → ∃n. 𝐮❨n❩ ≐ f.
 #f #H elim H -f
 [ /3 width=2 by pr_isi_inv_uni, ex_intro/
 | #f #_ #g #H * /3 width=6 by pr_eq_next, ex_intro/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma
index 3ca8053d8..9e06b6fe7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_nexts.ma".
 
 (*** nexts_eq_repl *)
 lemma pr_nexts_eq_repl (n):
-      pr_eq_repl (λf1,f2. ↑*[n] f1 ≡ ↑*[n] f2).
+      pr_eq_repl (λf1,f2. ↑*[n] f1 ≐ ↑*[n] f2).
 #n @(nat_ind_succ … n) -n
 /3 width=5 by pr_eq_next/
 qed.
@@ -29,8 +29,8 @@ qed.
 (* Inversions with pr_eq ****************************************************)
 
 lemma pr_eq_inv_nexts_push_bi (f1) (f2) (n1) (n2):
-      ↑*[n1] ⫯f1 ≡ ↑*[n2] ⫯f2 →
-      ∧∧ n1 = n2 & f1 ≡ f2.
+      ↑*[n1] ⫯f1 ≐ ↑*[n2] ⫯f2 →
+      ∧∧ n1 = n2 & f1 ≐ f2.
 #f1 #f2
 #n1 @(nat_ind_succ … n1) -n1 [| #n1 #IH ]
 #n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ]
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
index 010fa0548..29620d121 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
@@ -38,7 +38,7 @@ lemma pr_pat_eq_repl_fwd (i1) (i2):
 #i1 #i2 @pr_eq_repl_sym /2 width=3 by pr_pat_eq_repl_back/
 qed-.
 
-lemma pr_pat_eq (f): ⫯f ≡ f → ∀i. @❨i,f❩ ≘ i.
+lemma pr_pat_eq (f): ⫯f ≐ f → ∀i. @❨i,f❩ ≘ i.
 #f #Hf #i elim i -i
 [ /3 width=3 by pr_pat_eq_repl_back, pr_pat_refl/
 | /3 width=7 by pr_pat_eq_repl_back, pr_pat_push/
@@ -48,7 +48,7 @@ qed.
 (* Inversions with pr_eq ****************************************************)
 
 corec lemma pr_pat_inv_eq (f):
-            (∀i. @❨i,f❩ ≘ i) → ⫯f ≡ f.
+            (∀i. @❨i,f❩ ≘ i) → ⫯f ≐ f.
 #Hf
 lapply (Hf (𝟏)) #H
 lapply (pr_pat_des_id … H) -H #H
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma
index a63fb9355..013468796 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma
@@ -27,6 +27,6 @@ lemma pr_pat_id (i): @❨i,𝐢❩ ≘ i.
 
 (*** id_inv_at *)
 lemma pr_pat_inv_id (f):
-      (∀i. @❨i,f❩ ≘ i) → 𝐢 ≡ f.
+      (∀i. @❨i,f❩ ≘ i) → 𝐢 ≐ f.
 /3 width=1 by pr_pat_inv_eq, pr_id_eq/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma
index 81dfaeecd..eaaaf0501 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma
@@ -32,7 +32,7 @@ qed.
 
 (* Note: this requires ↑ on third n2 *)
 (*** at_tls *)
-lemma pr_pat_tls (n2) (f): ⫯⫰*[↑n2]f ≡ ⫰*[n2]f → ∃i1. @❨i1,f❩ ≘ ↑n2.
+lemma pr_pat_tls (n2) (f): ⫯⫰*[↑n2]f ≐ ⫰*[n2]f → ∃i1. @❨i1,f❩ ≘ ↑n2.
 #n2 @(nat_ind_succ … n2) -n2
 [ /4 width=4 by pr_pat_eq_repl_back, pr_pat_refl, ex_intro/
 | #n2 #IH #f <pr_tls_swap <pr_tls_swap in ⊢ (??%→?); #H
@@ -65,7 +65,7 @@ qed-.
 (* Note: this requires ↑ on first n2 *)
 (*** at_inv_tls *)
 lemma pr_pat_inv_succ_dx_tls (n2) (i1) (f):
-      @❨i1,f❩ ≘ ↑n2 → ⫯⫰*[↑n2]f ≡ ⫰*[n2]f.
+      @❨i1,f❩ ≘ ↑n2 → ⫯⫰*[↑n2]f ≐ ⫰*[n2]f.
 #n2 @(nat_ind_succ … n2) -n2
 [ #i1 #f #Hf elim (pr_pat_inv_unit_dx … Hf) -Hf // #g #H1 #H destruct
   /2 width=1 by pr_eq_refl/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pushs_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pushs_eq.ma
index 11f4036a2..dacdb9b69 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pushs_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pushs_eq.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_pushs.ma".
 
 (*** pushs_eq_repl *)
 lemma pr_pushs_eq_repl (n):
-      pr_eq_repl (λf1,f2. ⫯*[n] f1 ≡ ⫯*[n] f2).
+      pr_eq_repl (λf1,f2. ⫯*[n] f1 ≐ ⫯*[n] f2).
 #n @(nat_ind_succ … n) -n
 /3 width=5 by pr_eq_push/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma
index 383ad127f..aa826268e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma
@@ -56,5 +56,5 @@ qed-.
 
 (*** sle_refl_eq *)
 lemma pr_sle_refl_eq:
-      ∀f1,f2. f1 ≡ f2 → f1 ⊆ f2.
+      ∀f1,f2. f1 ≐ f2 → f1 ⊆ f2.
 /2 width=3 by pr_sle_eq_repl_back_dx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma
index bc307df7e..98eaf1ed1 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma
@@ -66,13 +66,13 @@ qed-.
 
 (*** sor_isid_inv_sn *)
 lemma pr_sor_inv_isi_sn:
-      ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❨f1❩ → f2 ≡ f.
+      ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❨f1❩ → f2 ≐ f.
 /3 width=4 by pr_sor_isi_sn, pr_sor_mono/
 qed-.
 
 (*** sor_isid_inv_dx *)
 lemma pr_sor_inv_isi_dx:
-      ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❨f2❩ → f1 ≡ f.
+      ∀f1,f2,f. f1 ⋓ f2 ≘ f → 𝐈❨f2❩ → f1 ≐ f.
 /3 width=4 by pr_sor_isi_dx, pr_sor_mono/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma
index ef667fd7e..c52154795 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_sor.ma".
 
 (*** sor_mono *)
 corec theorem pr_sor_mono:
-              ∀f1,f2,x,y. f1 ⋓ f2 ≘ x → f1 ⋓ f2 ≘ y → x ≡ y.
+              ∀f1,f2,x,y. f1 ⋓ f2 ≘ x → f1 ⋓ f2 ≘ y → x ≐ y.
 #f1 #f2 #x #y * -f1 -f2 -x
 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #H
 [ cases (pr_sor_inv_push_bi … H … H1 H2)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq.ma
index 03c413e46..fe7e7b3a8 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq.ma
@@ -27,7 +27,7 @@ qed.
 
 (*** tl_eq_repl *)
 lemma pr_tl_eq_repl:
-      pr_eq_repl … (λf1,f2. ⫰f1 ≡ ⫰f2).
+      pr_eq_repl … (λf1,f2. ⫰f1 ≐ ⫰f2).
 #f1 #f2 * -f1 -f2 //
 qed.
 
@@ -35,9 +35,9 @@ qed.
 
 (*** eq_inv_gen *)
 lemma pr_eq_inv_gen (g1) (g2):
-      g1 ≡ g2 →
-      ∨∨ ∧∧ ⫰g1 ≡ ⫰g2 & ⫯⫰g1 = g1 & ⫯⫰g2 = g2
-       | ∧∧ ⫰g1 ≡ ⫰g2 & ↑⫰g1 = g1 & ↑⫰g2 = g2.
+      g1 ≐ g2 →
+      ∨∨ ∧∧ ⫰g1 ≐ ⫰g2 & ⫯⫰g1 = g1 & ⫯⫰g2 = g2
+       | ∧∧ ⫰g1 ≐ ⫰g2 & ↑⫰g1 = g1 & ↑⫰g2 = g2.
 #g1 #g2 * -g1 -g2 #f1 #f2 #g1 #g2 #f * *
 /3 width=1 by and3_intro, or_introl, or_intror/
 qed-.
@@ -46,8 +46,8 @@ qed-.
 
 (*** pr_eq_inv_px *)
 lemma pr_eq_inv_push_sn (g1) (g2):
-      g1 ≡ g2 → ∀f1. ⫯f1 = g1 →
-      ∧∧ f1 ≡ ⫰g2 & ⫯⫰g2 = g2.
+      g1 ≐ g2 → ∀f1. ⫯f1 = g1 →
+      ∧∧ f1 ≐ ⫰g2 & ⫯⫰g2 = g2.
 #g1 #g2 #H #f1 #Hf1
 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
 [ /2 width=1 by conj/
@@ -57,8 +57,8 @@ qed-.
 
 (*** pr_eq_inv_nx *)
 lemma pr_eq_inv_next_sn (g1) (g2):
-      g1 ≡ g2 → ∀f1. ↑f1 = g1 →
-      ∧∧ f1 ≡ ⫰g2 & ↑⫰g2 = g2.
+      g1 ≐ g2 → ∀f1. ↑f1 = g1 →
+      ∧∧ f1 ≐ ⫰g2 & ↑⫰g2 = g2.
 #g1 #g2 #H #f1 #Hf1
 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
 [ elim (eq_inv_pr_push_next … Hg1)
@@ -68,8 +68,8 @@ qed-.
 
 (*** pr_eq_inv_xp *)
 lemma pr_eq_inv_push_dx (g1) (g2):
-      g1 ≡ g2 → ∀f2. ⫯f2 = g2 →
-      ∧∧ ⫰g1 ≡ f2 & ⫯⫰g1 = g1.
+      g1 ≐ g2 → ∀f2. ⫯f2 = g2 →
+      ∧∧ ⫰g1 ≐ f2 & ⫯⫰g1 = g1.
 #g1 #g2 #H #f2 #Hf2
 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
 [ /2 width=1 by conj/
@@ -79,8 +79,8 @@ qed-.
 
 (*** pr_eq_inv_xn *)
 lemma pr_eq_inv_next_dx (g1) (g2):
-      g1 ≡ g2 → ∀f2. ↑f2 = g2 →
-      ∧∧ ⫰g1 ≡ f2 & ↑⫰g1 = g1.
+      g1 ≐ g2 → ∀f2. ↑f2 = g2 →
+      ∧∧ ⫰g1 ≐ f2 & ↑⫰g1 = g1.
 #g1 #g2 #H #f2 #Hf2
 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
 [ elim (eq_inv_pr_push_next … Hg2)
@@ -90,7 +90,7 @@ qed-.
 
 (*** pr_eq_inv_pp *)
 lemma pr_eq_inv_push_bi (g1) (g2):
-      g1 ≡ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ≡ f2.
+      g1 ≐ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ≐ f2.
 #g1 #g2 #H #f1 #f2 #H1
 elim (pr_eq_inv_push_sn … H … H1) -g1 #Hx2 * #H
 lapply (eq_inv_pr_push_bi … H) -H //
@@ -98,7 +98,7 @@ qed-.
 
 (*** pr_eq_inv_nn *)
 lemma pr_eq_inv_next_bi (g1) (g2):
-      g1 ≡ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ≡ f2.
+      g1 ≐ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ≐ f2.
 #g1 #g2 #H #f1 #f2 #H1
 elim (pr_eq_inv_next_sn … H … H1) -g1 #Hx2 * #H
 lapply (eq_inv_pr_next_bi … H) -H //
@@ -106,7 +106,7 @@ qed-.
 
 (*** pr_eq_inv_pn *)
 lemma pr_eq_inv_push_next (g1) (g2):
-      g1 ≡ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → ⊥.
+      g1 ≐ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → ⊥.
 #g1 #g2 #H #f1 #f2 #H1
 elim (pr_eq_inv_push_sn … H … H1) -g1 #Hx2 * #H
 elim (eq_inv_pr_next_push … H)
@@ -114,7 +114,7 @@ qed-.
 
 (*** pr_eq_inv_np *)
 lemma pr_eq_inv_next_push (g1) (g2):
-      g1 ≡ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → ⊥.
+      g1 ≐ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → ⊥.
 #g1 #g2 #H #f1 #f2 #H1
 elim (pr_eq_inv_next_sn … H … H1) -g1 #Hx2 * #H
 elim (eq_inv_pr_push_next … H)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma
index 94592fdfd..43b69b3f0 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma
@@ -29,9 +29,9 @@ corec theorem pr_eq_trans: Transitive … pr_eq.
 qed-.
 
 (*** eq_canc_sn *)
-theorem pr_eq_canc_sn (f2): pr_eq_repl_back (λf. f ≡ f2).
+theorem pr_eq_canc_sn (f2): pr_eq_repl_back (λf. f ≐ f2).
 /3 width=3 by pr_eq_trans, pr_eq_sym/ qed-.
 
 (*** eq_canc_dx *)
-theorem pr_eq_canc_dx (f1): pr_eq_repl_fwd (λf. f1 ≡ f).
+theorem pr_eq_canc_dx (f1): pr_eq_repl_fwd (λf. f1 ≐ f).
 /3 width=5 by pr_eq_canc_sn, pr_eq_repl_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_eq.ma
index f3b5bc74d..ce9fc0ad0 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_eq.ma
@@ -21,6 +21,6 @@ include "ground/relocation/pr_tls.ma".
 
 (*** tls_eq_repl *)
 lemma pr_tls_eq_repl (n):
-      pr_eq_repl (λf1,f2. ⫰*[n] f1 ≡ ⫰*[n] f2).
+      pr_eq_repl (λf1,f2. ⫰*[n] f1 ≐ ⫰*[n] f2).
 #n @(nat_ind_succ … n) -n /3 width=1 by pr_tl_eq_repl/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_nexts_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_nexts_eq.ma
index 004b20fe7..b17dc66ee 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_nexts_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_nexts_eq.ma
@@ -21,8 +21,8 @@ include "ground/relocation/pr_tls_eq.ma".
 
 (*** eq_inv_nexts_sn *)
 lemma pr_eq_inv_nexts_sn (n):
-      ∀f1,g2. ↑*[n] f1 ≡ g2 →
-      ∧∧ f1 ≡ ⫰*[n]g2 & ↑*[n]⫰*[n]g2 = g2.
+      ∀f1,g2. ↑*[n] f1 ≐ g2 →
+      ∧∧ f1 ≐ ⫰*[n]g2 & ↑*[n]⫰*[n]g2 = g2.
 #n @(nat_ind_succ … n) -n /2 width=1 by conj/
 #n #IH #f1 #g2 #H
 elim (pr_eq_inv_next_sn … H) -H [|*: // ] #Hf10 *
@@ -32,8 +32,8 @@ qed-.
 
 (*** eq_inv_nexts_dx *)
 lemma pr_eq_inv_nexts_dx (n):
-      ∀f2,g1. g1 ≡ ↑*[n] f2 →
-      ∧∧ ⫰*[n]g1 ≡ f2 & ↑*[n]⫰*[n]g1 = g1.
+      ∀f2,g1. g1 ≐ ↑*[n] f2 →
+      ∧∧ ⫰*[n]g1 ≐ f2 & ↑*[n]⫰*[n]g1 = g1.
 #n @(nat_ind_succ … n) -n /2 width=1 by conj/
 #n #IH #f2 #g1 #H
 elim (pr_eq_inv_next_dx … H) -H [|*: // ] #Hf02 *
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_pushs_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_pushs_eq.ma
index 31055e9ad..37a657203 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_pushs_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_pushs_eq.ma
@@ -21,8 +21,8 @@ include "ground/relocation/pr_pushs.ma".
 
 (*** eq_inv_pushs_sn *)
 lemma pr_eq_inv_pushs_sn (n):
-      ∀f1,g2. ⫯*[n] f1 ≡ g2 →
-      ∧∧ f1 ≡ ⫰*[n]g2 & ⫯*[n]⫰*[n]g2 = g2.
+      ∀f1,g2. ⫯*[n] f1 ≐ g2 →
+      ∧∧ f1 ≐ ⫰*[n]g2 & ⫯*[n]⫰*[n]g2 = g2.
 #n @(nat_ind_succ … n) -n /2 width=1 by conj/
 #n #IH #f1 #g2 #H
 elim (pr_eq_inv_push_sn … H) -H [|*: // ] #Hf10 *
@@ -32,8 +32,8 @@ qed-.
 
 (*** eq_inv_pushs_dx *)
 lemma pr_eq_inv_pushs_dx (n):
-      ∀f2,g1. g1 ≡ ⫯*[n] f2 →
-      ∧∧ ⫰*[n]g1 ≡ f2 & ⫯*[n]⫰*[n]g1 = g1.
+      ∀f2,g1. g1 ≐ ⫯*[n] f2 →
+      ∧∧ ⫰*[n]g1 ≐ f2 & ⫯*[n]⫰*[n]g1 = g1.
 #n @(nat_ind_succ … n) -n /2 width=1 by conj/
 #n #IH #f2 #g1 #H
 elim (pr_eq_inv_push_dx … H) -H [|*: // ] #Hf02 *
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_uni_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_uni_eq.ma
index 44e989101..f705ca84b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_uni_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_uni_eq.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_uni.ma".
 (* Inversions with pr_eq ****************************************************)
 
 (*** uni_inv_push_dx *)
-lemma pr_eq_inv_uni_push (n) (g):  𝐮❨n❩ ≡ ⫯g → ∧∧ 𝟎 = n & 𝐢 ≡ g.
+lemma pr_eq_inv_uni_push (n) (g):  𝐮❨n❩ ≐ ⫯g → ∧∧ 𝟎 = n & 𝐢 ≐ g.
 #n @(nat_ind_succ … n) -n 
 [ /3 width=5 by pr_eq_inv_push_bi, conj/
 | #n #_ #f <pr_uni_succ #H elim (pr_eq_inv_next_push … H) -H //
@@ -29,11 +29,11 @@ lemma pr_eq_inv_uni_push (n) (g):  𝐮❨n❩ ≡ ⫯g → ∧∧ 𝟎 = n & 
 qed-.
 
 (*** uni_inv_push_sn *)
-lemma pr_eq_inv_push_uni (n) (g): ⫯g ≡ 𝐮❨n❩ → ∧∧ 𝟎 = n & 𝐢 ≡ g.
+lemma pr_eq_inv_push_uni (n) (g): ⫯g ≐ 𝐮❨n❩ → ∧∧ 𝟎 = n & 𝐢 ≐ g.
 /3 width=1 by pr_eq_inv_uni_push, pr_eq_sym/ qed-.
 
 (*** uni_inv_next_dx *)
-lemma pr_eq_inv_uni_next (n) (g): 𝐮❨n❩ ≡ ↑g → ∧∧ 𝐮❨↓n❩ ≡ g & ↑↓n = n.
+lemma pr_eq_inv_uni_next (n) (g): 𝐮❨n❩ ≐ ↑g → ∧∧ 𝐮❨↓n❩ ≐ g & ↑↓n = n.
 #n @(nat_ind_succ … n) -n
 [ #g <pr_uni_zero <pr_id_unfold #H elim (pr_eq_inv_push_next … H) -H //
 | #n #_ #g <pr_uni_succ /3 width=5 by pr_eq_inv_next_bi, conj/
@@ -41,16 +41,16 @@ lemma pr_eq_inv_uni_next (n) (g): 𝐮❨n❩ ≡ ↑g → ∧∧ 𝐮❨↓n❩
 qed-.
 
 (*** uni_inv_next_sn *)
-lemma pr_eq_inv_next_uni (n) (g): ↑g ≡ 𝐮❨n❩ → ∧∧ 𝐮❨↓n❩ ≡ g & ↑↓n = n.
+lemma pr_eq_inv_next_uni (n) (g): ↑g ≐ 𝐮❨n❩ → ∧∧ 𝐮❨↓n❩ ≐ g & ↑↓n = n.
 /3 width=1 by pr_eq_inv_uni_next, pr_eq_sym/ qed-.
 
 (* Inversions with pr_id and pr_eq ******************************************)
 
 (*** uni_inv_id_dx *)
-lemma pr_eq_inv_uni_id (n): 𝐮❨n❩ ≡ 𝐢 → 𝟎 = n.
+lemma pr_eq_inv_uni_id (n): 𝐮❨n❩ ≐ 𝐢 → 𝟎 = n.
 #n <pr_id_unfold #H elim (pr_eq_inv_uni_push … H) -H //
 qed-.
 
 (*** uni_inv_id_sn *)
-lemma pr_eq_inv_id_uni (n):  𝐢 ≡ 𝐮❨n❩ → 𝟎 = n.
+lemma pr_eq_inv_id_uni (n):  𝐢 ≐ 𝐮❨n❩ → 𝟎 = n.
 /3 width=1 by pr_eq_inv_uni_id, pr_eq_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
index 663dfc9b6..4c8586c31 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
@@ -89,7 +89,7 @@ lemma after_inv_const: ∀f2,f1,f,p1,p.
 ]
 qed-.
 
-lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
+lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≐ f.
 /2 width=4 by gr_after_mono/ qed-.
 
 (* Forward lemmas on after (specific) *****************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma
index 869486b4a..262fe6167 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma
@@ -19,7 +19,7 @@ include "ground/relocation/tr_nexts.ma".
 
 (* Constructions with pr_eq and stream_eq ***********************************)
 
-corec lemma eq_tr_inj_bi (f1) (f2): f1 ≗ f2 → 𝐭❨f1❩ ≡ 𝐭❨f2❩.
+corec lemma eq_tr_inj_bi (f1) (f2): f1 ≗ f2 → 𝐭❨f1❩ ≐ 𝐭❨f2❩.
 * -f1 -f2 #p1 #p2 #f1 #f2 * -p2 #H
 cases p1 -p1
 [ @pr_eq_push /2 width=5 by/
@@ -31,7 +31,7 @@ qed.
 
 (* Inversions with pr_eq and stream_eq **************************************)
 
-corec lemma eq_inv_tr_inj_bi (f1) (f2): 𝐭❨f1❩ ≡ 𝐭❨f2❩ → f1 ≗ f2.
+corec lemma eq_inv_tr_inj_bi (f1) (f2): 𝐭❨f1❩ ≐ 𝐭❨f2❩ → f1 ≗ f2.
 cases f1 -f1 #p1 #f1 cases f2 -f2 #p2 #f2
 cases tr_inj_unfold cases tr_inj_unfold #H
 cases (pr_eq_inv_nexts_push_bi … H) -H #H1 #H2
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 2b655f20c..528c13cf4 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -60,7 +60,7 @@ table {
           [ "pr_nexts ( ↑*[?]? )" "pr_nexts_eq" * ]
           [ "pr_pushs ( ⫯*[?]? )" "pr_pushs_eq" * ]
           [ "pr_tl ( â«°? )" "pr_tl_eq" "pr_tl_eq_eq" * ]
-          [ "pr_eq ( ? ≡ ? )" * ]
+          [ "pr_eq ( ? ≐ ? )" * ]
           [ "pr_map ( ⫯? ) ( ↑? )" * ]
         }
       ]
@@ -143,7 +143,7 @@ table {
       [ { "" * } {
           [ "bool ( Ⓕ ) ( Ⓣ )" "bool_or" "bool_and" * ]
           [ "ltc" "ltc_ctc" * ]
-          [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ]
+          [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ⊜{?,?} ? )" "star" "lstar_2a" * ]
         }
       ]
     }
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma b/matita/matita/contribs/lambdadelta/static_2/notation/relations/ideq_2.ma
similarity index 93%
rename from matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma
rename to matita/matita/contribs/lambdadelta/static_2/notation/relations/ideq_2.ma
index 8ade3ee43..ae7999266 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/notation/relations/ideq_2.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GROUND NOTATION **********************************************************)
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
 notation "hvbox( f1 ≡ break term 46 f2 )"
   non associative with precedence 45
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma
index 6b4a58e82..be5f31895 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/relations/ideq_2.ma".
+include "static_2/notation/relations/ideq_2.ma".
 include "static_2/syntax/teqg.ma".
 
 (* SYNTACTIC EQUIVALENCE ON TERMS *******************************************)
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 4dd5b0f5e..94f34fb10 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1512,7 +1512,7 @@ let predefined_classes = [
  ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ];
  ["+"; "⨭"; "⨮"; "⨁"; "⊕"; "⊞"; ];
  ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ];
- ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ];  
+ ["="; "≝"; "≡"; "≘"; "⊜"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ];
  ["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
  ["⇒"; "⤇"; "➾"; "⇨"; "⬀"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ;
  ["^"; "↑"; "⇡"; "↥"; "▵"; ] ;
-- 
2.39.2