From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Wed, 25 Apr 2018 11:25:19 +0000 (+0200)
Subject: update in ground_2 and basic_2
X-Git-Tag: make_still_working~338
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=54c4e854515cbcb1376881e9aedad006bf6545f2

update in ground_2 and basic_2

+ old and unused definition llstar replaced with new definition ltc to appear in cpms
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_lstar.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_lstar.etc
new file mode 100644
index 000000000..47da596ad
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_lstar.etc
@@ -0,0 +1,22 @@
+include "ground_2/lib/lstar.ma".
+
+(* Basic_2A1: was: d_liftable_llstar *)
+lemma d2_liftable_sn_llstar: ∀C,S,R. d_liftable2_sn C S R → ∀d. d_liftable2_sn C S (llstar … R d).
+#C #S #R #HR #d #K #T1 #T2 #H @(lstar_ind_r … d T2 H) -d -T2
+[ #b #f #L #_ #U1 #HTU1 -HR -b -K /2 width=3 by ex2_intro/
+| #l #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1
+  elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1
+  elim (HR … HT2 … HLK … HTU) -T /3 width=5 by lstar_dx, ex2_intro/
+]
+qed-.
+
+(* Basic_2A1: was: d_deliftable_sn_llstar *)
+lemma d2_deliftable_sn_llstar: ∀C,S,R. d_deliftable2_sn C S R →
+                               ∀d. d_deliftable2_sn C S (llstar … R d).
+#C #S #R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2
+[ /2 width=3 by lstar_O, ex2_intro/
+| #l #U #U2 #_ #HU2 #IHU1 #b #f #K #HLK #T1 #HTU1
+  elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
+  elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ctc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ctc.ma
new file mode 100644
index 000000000..cc485711c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ctc.ma
@@ -0,0 +1,72 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lib/star.ma".
+include "basic_2/relocation/lreq_lreq.ma".
+
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+
+(* Properties with contextual transitive closure ****************************)
+
+(* Basic_2A1: was: d_liftable_LTC *)
+lemma d2_liftable_sn_CTC: ∀C,S,R. d_liftable2_sn C S R → d_liftable2_sn C S (CTC … R).
+#C #S #R #HR #K #T1 #T2 #H elim H -T2
+[ #T2 #HT12 #b #f #L #HLK #U1 #HTU1
+  elim (HR … HT12 … HLK … HTU1) /3 width=3 by inj, ex2_intro/
+| #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1
+  elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1
+  elim (HR … HT2 … HLK … HTU) -HR -K -T /3 width=5 by step, ex2_intro/
+]
+qed-.
+
+(* Basic_2A1: was: d_deliftable_sn_LTC *)
+lemma d2_deliftable_sn_CTC: ∀C,S,R. d_deliftable2_sn C S R → d_deliftable2_sn C S (CTC … R).
+#C #S #R #HR #L #U1 #U2 #H elim H -U2
+[ #U2 #HU12 #b #f #K #HLK #T1 #HTU1
+  elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3 by inj, ex2_intro/
+| #U #U2 #_ #HU2 #IHU1 #b #f #K #HLK #T1 #HTU1
+  elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
+  elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by step, ex2_intro/
+]
+qed-.
+
+lemma co_dropable_sn_CTC: ∀R. co_dropable_sn R → co_dropable_sn (CTC … R).
+#R #HR #b #f #L1 #K1 #HLK1 #Hf #f2 #L2 #H elim H -L2
+[ #L2 #HL12 #f1 #H elim (HR … HLK1 … Hf … HL12 … H) -HR -Hf -f2 -L1
+  /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 #IH #f1 #H elim (IH … H) -IH
+  #K #HK1 #HLK elim (HR … HLK … HL2 … H) -HR -f2 -L
+  /3 width=3 by step, ex2_intro/
+]
+qed-.
+
+lemma co_dropable_dx_CTC: ∀R. co_dropable_dx R → co_dropable_dx (CTC … R).
+#R #HR #f2 #L1 #L2 #H elim H -L2
+[ #L2 #HL12 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL12 … HLK2 … Hf … Hf2) -HR -Hf -f2 -L2
+  /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 #IHL1 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL2 … HLK2 … Hf … Hf2) -HR -L2
+  #K #HLK #HK2 elim (IHL1 … HLK … Hf … Hf2) -Hf -f2 -L
+  /3 width=5 by step, ex2_intro/
+]
+qed-.
+
+lemma co_dedropable_sn_CTC: ∀R. co_dedropable_sn R → co_dedropable_sn (CTC … R).
+#R #HR #b #f #L1 #K1 #HLK1 #f1 #K2 #H elim H -K2
+[ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -f1 -K1
+  /3 width=4 by inj, ex3_intro/
+| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1
+  #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -f1 -K
+  /3 width=6 by lreq_trans, step, ex3_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma
deleted file mode 100644
index dadccae4f..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma
+++ /dev/null
@@ -1,94 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/lib/star.ma".
-include "ground_2/lib/lstar.ma".
-include "basic_2/relocation/lreq_lreq.ma".
-
-(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
-
-(* Properties with reflexive and transitive closure *************************)
-
-(* Basic_2A1: was: d_liftable_LTC *)
-lemma d2_liftable_sn_CTC: ∀C,S,R. d_liftable2_sn C S R → d_liftable2_sn C S (CTC … R).
-#C #S #R #HR #K #T1 #T2 #H elim H -T2
-[ #T2 #HT12 #b #f #L #HLK #U1 #HTU1
-  elim (HR … HT12 … HLK … HTU1) /3 width=3 by inj, ex2_intro/
-| #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1
-  elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1
-  elim (HR … HT2 … HLK … HTU) -HR -K -T /3 width=5 by step, ex2_intro/
-]
-qed-.
-
-(* Basic_2A1: was: d_deliftable_sn_LTC *)
-lemma d2_deliftable_sn_CTC: ∀C,S,R. d_deliftable2_sn C S R → d_deliftable2_sn C S (CTC … R).
-#C #S #R #HR #L #U1 #U2 #H elim H -U2
-[ #U2 #HU12 #b #f #K #HLK #T1 #HTU1
-  elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3 by inj, ex2_intro/
-| #U #U2 #_ #HU2 #IHU1 #b #f #K #HLK #T1 #HTU1
-  elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
-  elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by step, ex2_intro/
-]
-qed-.
-
-lemma co_dropable_sn_TC: ∀R. co_dropable_sn R → co_dropable_sn (CTC … R).
-#R #HR #b #f #L1 #K1 #HLK1 #Hf #f2 #L2 #H elim H -L2
-[ #L2 #HL12 #f1 #H elim (HR … HLK1 … Hf … HL12 … H) -HR -Hf -f2 -L1
-  /3 width=3 by inj, ex2_intro/
-| #L #L2 #_ #HL2 #IH #f1 #H elim (IH … H) -IH
-  #K #HK1 #HLK elim (HR … HLK … HL2 … H) -HR -f2 -L
-  /3 width=3 by step, ex2_intro/
-]
-qed-.
-
-(* Basic_2A1: was: d_liftable_llstar *)
-lemma d2_liftable_sn_llstar: ∀C,S,R. d_liftable2_sn C S R → ∀d. d_liftable2_sn C S (llstar … R d).
-#C #S #R #HR #d #K #T1 #T2 #H @(lstar_ind_r … d T2 H) -d -T2
-[ #b #f #L #_ #U1 #HTU1 -HR -b -K /2 width=3 by ex2_intro/
-| #l #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1
-  elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1
-  elim (HR … HT2 … HLK … HTU) -T /3 width=5 by lstar_dx, ex2_intro/
-]
-qed-.
-
-(* Basic_2A1: was: d_deliftable_sn_llstar *)
-lemma d2_deliftable_sn_llstar: ∀C,S,R. d_deliftable2_sn C S R →
-                               ∀d. d_deliftable2_sn C S (llstar … R d).
-#C #S #R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2
-[ /2 width=3 by lstar_O, ex2_intro/
-| #l #U #U2 #_ #HU2 #IHU1 #b #f #K #HLK #T1 #HTU1
-  elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
-  elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/
-]
-qed-.
-
-lemma co_dropable_dx_TC: ∀R. co_dropable_dx R → co_dropable_dx (CTC … R).
-#R #HR #f2 #L1 #L2 #H elim H -L2
-[ #L2 #HL12 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL12 … HLK2 … Hf … Hf2) -HR -Hf -f2 -L2
-  /3 width=3 by inj, ex2_intro/
-| #L #L2 #_ #HL2 #IHL1 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL2 … HLK2 … Hf … Hf2) -HR -L2
-  #K #HLK #HK2 elim (IHL1 … HLK … Hf … Hf2) -Hf -f2 -L
-  /3 width=5 by step, ex2_intro/
-]
-qed-.
-
-lemma co_dedropable_sn_TC: ∀R. co_dedropable_sn R → co_dedropable_sn (CTC … R).
-#R #HR #b #f #L1 #K1 #HLK1 #f1 #K2 #H elim H -K2
-[ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -f1 -K1
-  /3 width=4 by inj, ex3_intro/
-| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1
-  #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -f1 -K
-  /3 width=6 by lreq_trans, step, ex3_intro/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
index 87ff4a980..04a376981 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/drops_lstar.ma".
+include "basic_2/relocation/drops_ctc.ma".
 include "basic_2/rt_transition/cpx_drops.ma".
 include "basic_2/rt_computation/cpxs.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 11112816b..f6b46722c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -201,7 +201,7 @@ table {
    class "orange"
    [ { "relocation" * } {
         [ { "generic slicing" * } {
-             [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ]
+             [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_ctc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ]
           }
         ]
         [ { "generic relocation" * } {
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma
new file mode 100644
index 000000000..64fbae2e1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lib/relations.ma".
+
+(* FUNCTIONS ****************************************************************)
+
+definition left_identity (A:Type[0]) (f): predicate A ≝ λi. ∀a:A. a = f i a.
+
+definition right_identity (A:Type[0]) (f): predicate A ≝ λi. ∀a:A. a = f a i.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/logic.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/logic.ma
new file mode 100644
index 000000000..852e4e9ce
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/logic.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "basics/logic.ma".
+include "ground_2/notation/xoa/false_0.ma".
+include "ground_2/notation/xoa/true_0.ma".
+include "ground_2/notation/xoa/or_2.ma".
+include "ground_2/notation/xoa/and_2.ma".
+include "ground_2/xoa/xoa.ma".
+
+interpretation "logical false" 'false = False.
+
+interpretation "logical true" 'true = True.
+
+(* Logical properties missing in the basic library **************************)
+
+lemma commutative_and: ∀A,B. A ∧ B → B ∧ A.
+#A #B * /2 width=1 by conj/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/lstar.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/lstar.ma
deleted file mode 100644
index ae707f2b9..000000000
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/lstar.ma
+++ /dev/null
@@ -1,20 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "arithmetics/lstar.ma".
-
-(* PROPERTIES OF NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE ***************)
-
-definition llstar: ∀A:Type[0]. ∀B. (A→relation B) → nat → (A→relation B) ≝
-                   λA,B,R,l,a. lstar … (R a) l.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
new file mode 100644
index 000000000..27ef34de4
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma
@@ -0,0 +1,78 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lib/functions.ma".
+
+(* LABELLED TRANSITIVE CLOSURE **********************************************)
+
+inductive ltc (A:Type[0]) (f) (B) (R:relation3 A B B): relation3 A B B ≝
+| ltc_rc   : ∀a,b1,b2. R a b1 b2 → ltc … a b1 b2
+| ltc_trans: ∀a1,a2,b1,b,b2. ltc … a1 b1 b → ltc … a2 b b2 → ltc … (f a1 a2) b1 b2
+.
+
+(* Basic properties *********************************************************)
+
+lemma ltc_sn (A) (f) (B) (R): ∀a1,b1,b. R a1 b1 b →
+                              ∀a2,b2. ltc A f B R a2 b b2 → ltc … f … R (f a1 a2) b1 b2.
+/3 width=3 by ltc_rc, ltc_trans/ qed.
+
+lemma ltc_dx (A) (f) (B) (R): ∀a1,b1,b. ltc A f B R a1 b1 b →
+                              ∀a2,b2. R a2 b b2 → ltc … f … R (f a1 a2) b1 b2.
+/3 width=3 by ltc_rc, ltc_trans/ qed.
+
+(* Basic eliminators ********************************************************)
+
+lemma ltc_ind_sn (A) (f) (B) (R) (Q:relation2 A B) (b2): associative … f →
+                 (∀a,b1. R a b1 b2 → Q a b1) →
+                 (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
+                 ∀a,b1. ltc … f … R a b1 b2 → Q a b1.
+#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq … b2)
+#b0 #H elim H -a -b1 -b0 /2 width=2 by/
+#a1 #a2 #b1 #b #b0 #H #Hb2 #_
+generalize in match Hb2; generalize in match a2; -Hb2 -a2
+elim H -a1 -b1 -b /4 width=4 by ltc_trans/
+qed-.
+
+lemma ltc_ind_dx (A) (f) (B) (R) (Q:A→predicate B) (b1): associative … f →
+                 (∀a,b2. R a b1 b2 → Q a b2) →
+                 (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) →
+                 ∀a,b2. ltc … f … R a b1 b2 → Q a b2.
+#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq … b1)
+#b0 #H elim H -a -b0 -b2 /2 width=2 by/
+#a1 #a2 #b0 #b #b2 #Hb0 #H #IHb0 #_
+generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0 -Hb0 -a1
+elim H -a2 -b -b2 /4 width=4 by ltc_trans/
+qed-.
+
+(* Advanced elimiators with reflexivity *************************************)
+
+lemma ltc_ind_sn_refl (A) (i) (f) (B) (R) (Q:relation2 A B) (b2):
+                      associative … f → right_identity … f i → reflexive B (R i) →
+                      Q i b2 →
+                      (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
+                      ∀a,b1. ltc … f … R a b1 b2 → Q a b1.
+#A #i #f #B #R #Q #b2 #H1f #H2f #HR #IH1 #IH2 #a #b1 #H
+@(ltc_ind_sn … R … H1f … IH2 … H) -a -b1 -H1f #a #b1 #Hb12
+>(H2f a) -H2f /3 width=4 by ltc_rc/
+qed-.
+
+lemma ltc_ind_dx_refl (A) (i) (f) (B) (R) (Q:A→predicate B) (b1):
+                      associative … f → left_identity … f i → reflexive B (R i) →
+                      Q i b1 →
+                      (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) →
+                      ∀a,b2. ltc … f … R a b1 b2 → Q a b2.
+#A #i #f #B #R #Q #b1 #H1f #H2f #HR #IH1 #IH2 #a #b2 #H
+@(ltc_ind_dx … R … H1f … IH2 … H) -a -b2 -H1f #a #b2 #Hb12
+>(H2f a) -H2f /3 width=4 by ltc_rc/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
index 86be38640..af10dbb89 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma
@@ -13,10 +13,13 @@
 (**************************************************************************)
 
 include "basics/relations.ma".
-include "ground_2/xoa/xoa_props.ma".
+include "ground_2/lib/logic.ma".
 
 (* GENERIC RELATIONS ********************************************************)
 
+lemma insert_eq: ∀A,a. ∀Q1,Q2:predicate A. (∀a0. Q1 a0 → a = a0 → Q2 a0) → Q1 a → Q2 a.
+/2 width=1 by/ qed-.
+
 (* Inclusion ****************************************************************)
 
 definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝
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 090a67164..a7da5c2d0 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
@@ -55,7 +55,7 @@ table {
              [ "stream ( ? @ ? )" "stream_eq ( ? ≗ ? )" "stream_hdtl ( ⫰? )" "stream_tls ( ⫰*[?]? )" * ]
              [ "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ]
              [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ]
-             [ "relations ( ? ⊆ ? )" "star" "lstar" * ]
+             [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "star" "ltc" * ]
           }
         ]
      }
@@ -63,7 +63,7 @@ table {
    class "orange"
    [ { "generated logical decomposables" * } {
         [ { "" * } {
-             [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" "xoa_props ( ⊥ ) ( ⊤ )" * ]
+             [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" * ]
           }
         ]
      }
diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma
deleted file mode 100644
index 530c0e2b3..000000000
--- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma
+++ /dev/null
@@ -1,30 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "basics/logic.ma".
-include "ground_2/notation/xoa/false_0.ma".
-include "ground_2/notation/xoa/true_0.ma".
-include "ground_2/notation/xoa/or_2.ma".
-include "ground_2/notation/xoa/and_2.ma".
-include "ground_2/xoa/xoa.ma".
-
-interpretation "logical false" 'false = False.
-
-interpretation "logical true" 'true = True.
-
-(* Logical properties missing in the basic library **************************) 
-
-lemma commutative_and: ∀A,B. A ∧ B → B ∧ A.
-#A #B * /2 width=1 by conj/
-qed-.