From badd398f31309584efc39254e26b056683157a65 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 26 Jul 2012 14:53:37 +0000
Subject: [PATCH] - matita: reset_font_size () added after matita.conf.xml is
 read to set the font size specified by the user - lambda_delta: equivalence
 between normal forms irreducible terms proved (context-sensitive version)

---
 .../lambda_delta/basic_2/computation/xprs.ma  |  17 ++-
 .../basic_2/grammar/lenv_append.ma            |   1 +
 .../lambda_delta/basic_2/reducibility/cif.ma  |  71 ++++++++++++
 .../basic_2/reducibility/cif_append.ma        |  34 ++++++
 .../lambda_delta/basic_2/reducibility/cnf.ma  |  31 ++++-
 .../basic_2/reducibility/cnf_cif.ma           | 108 ++++++++++++++++++
 .../basic_2/reducibility/cnf_lift.ma          |  24 ++++
 .../lambda_delta/basic_2/reducibility/crf.ma  |  31 +++--
 .../basic_2/reducibility/crf_append.ma        |  53 +++++----
 .../lambda_delta/basic_2/reducibility/thnf.ma |   4 +-
 .../lambda_delta/basic_2/reducibility/tif.ma  |  54 ---------
 .../lambda_delta/basic_2/reducibility/tnf.ma  |  59 ----------
 .../basic_2/reducibility/tnf_tif.ma           |  74 ------------
 .../basic_2/substitution/ldrop.ma             |  17 ++-
 .../basic_2/substitution/ldrop_append.ma      |  42 +++++--
 .../basic_2/unfold/delift_lift.ma             |   2 +-
 .../lambda_delta/ground_2/xoa.conf.xml        |   1 +
 .../contribs/lambda_delta/ground_2/xoa.ma     |   8 ++
 .../lambda_delta/ground_2/xoa_notation.ma     |   6 +
 matita/matita/matita.ml                       |   3 +-
 20 files changed, 394 insertions(+), 246 deletions(-)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/cif.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/cif_append.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_cif.ma
 delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
 delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma
 delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma
index 2eb8903e1..c07de4dfd 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma
@@ -45,22 +45,19 @@ qed-.
 lemma xprs_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸*[g] T.
 /2 width=1/ qed.
 
-axiom xprs_strap1: ∀h,g,L,T1,T,T2.
+lemma xprs_strap1: ∀h,g,L,T1,T,T2.
                    ⦃h, L⦄ ⊢ T1 ➸*[g] T → ⦃h, L⦄ ⊢ T ➸[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2.
-(**) (* NTypeChecker failure
-/2 width=3/ qed.
-*)
-axiom xprs_strap2: ∀h,g,L,T1,T,T2.
+/2 width=3 by step/ qed. (**) (* NTypeChecker failure without trace *)
+
+lemma xprs_strap2: ∀h,g,L,T1,T,T2.
                    ⦃h, L⦄ ⊢ T1 ➸[g] T → ⦃h, L⦄ ⊢ T ➸*[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2.
-(**) (* NTypeChecker failure
-/2 width=3/ qed.
-*)
+/2 width=3 by TC_strap/ qed. (**) (* NTypeChecker failure without trace *)
+
 (* Basic inversion lemmas ***************************************************)
 (*
 axiom xprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U.
-(*
 #L #T #U #H @(xprs_ind_dx … H) -T //
 #T0 #T #H1T0 #_ #IHT #H2T0
 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
 qed-.
-*)*)
+*)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
index 336cd7b2f..a97908233 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
@@ -46,6 +46,7 @@ lemma append_inv_sn: ∀L1,L2,L. L1 @@ L = L2 @@ L → L1 = L2.
 #L #I #V #IHL #HL12 destruct /2 width=1/ (**) (* destruct does not simplify well *)
 qed.
 
+(* Note: lemma 750 *)
 lemma append_inv_dx: ∀L1,L2,L. L @@ L1 = L @@ L2 → L1 = L2.
 #L1 elim L1 -L1
 [ * normalize //
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cif.ma
new file mode 100644
index 000000000..0ea9d519b
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cif.ma
@@ -0,0 +1,71 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "basic_2/reducibility/crf.ma".
+
+(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
+
+definition cif: lenv → predicate term ≝ λL,T. L ⊢ 𝐑⦃T⦄ → ⊥.
+
+interpretation "context-sensitive irreducibility (term)"
+   'NotReducible L T = (cif L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cif_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐈⦃#i⦄ → ⊥.
+/3 width=3/ qed-.
+
+lemma cif_inv_ri2: ∀I,L,V,T. ri2 I → L ⊢ 𝐈⦃②{I}V.T⦄ → ⊥.
+/3 width=1/ qed-.
+
+lemma cif_inv_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
+                   L ⊢ 𝐈⦃V⦄ ∧ L.ⓑ{I}V ⊢ 𝐈⦃T⦄.
+/4 width=1/ qed-.
+
+lemma cif_inv_bind: ∀a,I,L,V,T. L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
+                    ∧∧ L ⊢ 𝐈⦃V⦄ & L.ⓑ{I}V ⊢ 𝐈⦃T⦄ & ib2 a I.
+#a * [ elim a -a ]
+[ #L #V #T #H elim (H ?) -H /3 width=1/
+|*: #L #V #T #H elim (cif_inv_ib2 … H) -H /2 width=1/ /3 width=1/
+]  
+qed-.
+
+lemma cif_inv_appl: ∀L,V,T. L ⊢ 𝐈⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄.
+#L #V #T #HVT @and3_intro /3 width=1/
+generalize in match HVT; -HVT elim T -T //
+* // #a * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
+qed-.
+
+lemma cif_inv_flat: ∀I,L,V,T. L ⊢ 𝐈⦃ⓕ{I}V.T⦄ →
+                    ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
+* #L #V #T #H
+[ elim (cif_inv_appl … H) -H /2 width=1/
+| elim (cif_inv_ri2 … H) -H /2 width=1/
+]
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma tif_atom: ∀I. ⋆ ⊢ 𝐈⦃⓪{I}⦄.
+/2 width=2 by trf_inv_atom/ qed.
+
+lemma cif_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃V⦄ → L.ⓑ{I}V ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄.
+#a #I #L #V #T #HI #HV #HT #H
+elim (crf_inv_ib2 … HI H) -HI -H /2 width=1/
+qed.
+
+lemma cif_appl: ∀L,V,T. L ⊢ 𝐈⦃V⦄ → L ⊢ 𝐈⦃T⦄ →  𝐒⦃T⦄ → L ⊢ 𝐈⦃ⓐV.T⦄.
+#L #V #T #HV #HT #H1 #H2
+elim (crf_inv_appl … H2) -H2 /2 width=1/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cif_append.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cif_append.ma
new file mode 100644
index 000000000..45fd178cf
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cif_append.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "basic_2/reducibility/crf_append.ma".
+include "basic_2/reducibility/cif.ma".
+
+(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
+
+(* Advanved properties ******************************************************)
+
+lemma cif_labst_last: ∀L,T,W. L ⊢ 𝐈⦃T⦄  → ⋆.ⓛW @@ L ⊢ 𝐈⦃T⦄.
+/3 width=2 by crf_inv_labst_last/ qed.
+
+lemma cif_tif: ∀T,W. ⋆ ⊢ 𝐈⦃T⦄ → ⋆.ⓛW ⊢ 𝐈⦃T⦄.
+/3 width=2 by crf_inv_trf/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cif_inv_labst_last: ∀L,T,W. ⋆.ⓛW @@ L ⊢ 𝐈⦃T⦄  → L ⊢ 𝐈⦃T⦄.
+/3 width=1/ qed-.
+
+lemma cif_inv_tif: ∀T,W. ⋆.ⓛW ⊢ 𝐈⦃T⦄  → ⋆ ⊢ 𝐈⦃T⦄.
+/3 width=1/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
index 41f363368..02bbcf87a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
@@ -20,7 +20,36 @@ definition cnf: lenv → predicate term ≝ λL. NF … (cpr L) (eq …).
 
 interpretation
    "context-sensitive normality (term)"
-   'Normal L T = (cnf L T). 
+   'Normal L T = (cnf L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cnf_inv_appl: ∀L,V,T. L ⊢ 𝐍⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐍⦃V⦄ & L ⊢ 𝐍⦃T⦄ & 𝐒⦃T⦄.
+#L #V1 #T1 #HVT1 @and3_intro
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
+  [ elim (lift_total V1 0 1) #V2 #HV12
+    lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
+  | lapply (H (ⓓ{a}V1.U1) ?) -H /3 width=1/ #H destruct
+]
+qed-.
+
+lemma cnf_inv_zeta: ∀L,V,T. L ⊢ 𝐍⦃+ⓓV.T⦄ → ⊥.
+#L #V #T #H elim (is_lift_dec T 0 1)
+[ * #U #HTU
+  lapply (H U ?) -H /3 width=3 by cpr_tpr, tpr_zeta/ #H destruct (**) (* auto too slow without trace *)
+  elim (lift_inv_pair_xy_y … HTU)
+| #HT
+  elim (tps_full (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12
+  lapply (H (+ⓓV.T2) ?) -H /3 width=3 by cpr_tpr, tpr_delta/ -HT2 #H destruct /3 width=2/ (**) (* auto too slow without trace *)
+]
+qed.
+
+lemma cnf_inv_tau: ∀L,V,T. L ⊢ 𝐍⦃ⓝV.T⦄ → ⊥.
+#L #V #T #H lapply (H T ?) -H /2 width=1/ #H
+@discr_tpair_xy_y //
+qed-.
 
 (* Basic properties *********************************************************)
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_cif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_cif.ma
new file mode 100644
index 000000000..33e52e1b7
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_cif.ma
@@ -0,0 +1,108 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "basic_2/substitution/tps_lift.ma".
+include "basic_2/unfold/tpss.ma".
+include "basic_2/reducibility/cif.ma".
+include "basic_2/reducibility/cnf_lift.ma".
+
+(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
+
+(* Main properties **********************************************************)
+
+lemma tps_cif_eq: ∀L,T1,T2,d,e. L ⊢ T1 ▶[d, e] T2 → L ⊢ 𝐈⦃T1⦄ → T1 = T2.
+#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
+[ //
+| #L #K #V #W #i #d #e #_ #_ #HLK #_ #H -d -e
+  elim (cif_inv_delta … HLK ?) //
+| #L #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H
+  elim (cif_inv_bind … H) -H #HV1 #HT1 * #H destruct
+  lapply (IHV12 … HV1) -IHV12 -HV1 #H destruct /3 width=1/
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H
+  elim (cif_inv_flat … H) -H #HV1 #HT1 #_ #_ /3 width=1/
+]
+qed.
+
+lemma tpss_cif_eq: ∀L,T1,T2,d,e. L ⊢ T1 ▶*[d, e] T2 → L ⊢ 𝐈⦃T1⦄ → T1 = T2.
+#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1 #HT1
+lapply (IHT1 HT1) -IHT1 #H destruct /2 width=5/
+qed.
+
+lemma tpr_cif_eq: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ 𝐈⦃T1⦄ → T1 = T2.
+#T1 #T2 #H elim H -T1 -T2
+[ //
+| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #L #H
+  [ elim (cif_inv_appl … H) -H #HV1 #HT1 #_
+    >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
+  | elim (cif_inv_ri2 … H) /2 width=1/
+  ]
+| #a #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #L #H
+  elim (cif_inv_appl … H) -H #_ #_ #H
+  elim (simple_inv_bind … H)
+| #a * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #L #H
+  [ lapply (tps_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+    elim (cif_inv_bind … H) -H #HV1 #HT1 * #H destruct
+    lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
+    lapply (IHT1 … HT1) -IHT1 #H destruct
+    lapply (tps_cif_eq … HT2 ?) -HT2 //
+  | <(tps_inv_refl_SO2 … HT2 ?) -HT2 //
+    elim (cif_inv_ib2 … H) -H /2 width=1/ /3 width=2/
+  ]
+| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #L #H
+  elim (cif_inv_appl … H) -H #_ #_ #H
+  elim (simple_inv_bind … H)
+| #V1 #T1 #T #T2 #_ #_ #_ #L #H
+  elim (cif_inv_ri2 … H) /2 width=1/
+| #V1 #T1 #T2 #_ #_ #L #H
+  elim (cif_inv_ri2 … H) /2 width=1/
+]
+qed.
+
+lemma cpr_cif_eq: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ 𝐈⦃T1⦄ → T1 = T2.
+#L #T1 #T2 * #T0 #HT10 #HT02 #HT1
+lapply (tpr_cif_eq … HT10 … HT1) -HT10 #H destruct /2 width=5/
+qed.
+
+theorem cif_cnf: ∀L,T. L ⊢ 𝐈⦃T⦄ → L ⊢ 𝐍⦃T⦄.
+/3 width=3/ qed.
+
+(* Note: this property is unusual *)
+lemma cnf_crf_false: ∀L,T. L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ⊥.
+#L #T #H elim H -L -T
+[ #L #K #V #i #HLK #H
+  elim (cnf_inv_delta … HLK H)
+| #L #V #T #_ #IHV #H
+  elim (cnf_inv_appl … H) -H /2 width=1/
+| #L #V #T #_ #IHT #H
+  elim (cnf_inv_appl … H) -H /2 width=1/
+| #I #L #V #T * #H1 #H2 destruct
+  [ elim (cnf_inv_zeta … H2)
+  | elim (cnf_inv_tau … H2)
+  ]
+|5,6: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
+  [1,3: elim (cnf_inv_abbr … H2) -H2 /2 width=1/
+  |*: elim (cnf_inv_abst … H2) -H2 /2 width=1/
+  ]
+| #a #L #V #W #T #H
+  elim (cnf_inv_appl … H) -H #_ #_ #H
+  elim (simple_inv_bind … H)
+| #a #L #V #W #T #H 
+  elim (cnf_inv_appl … H) -H #_ #_ #H
+  elim (simple_inv_bind … H)
+]
+qed.
+
+theorem cnf_cif: ∀L,T. L ⊢ 𝐍⦃T⦄ → L ⊢ 𝐈⦃T⦄.
+/2 width=4/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma
index 6c980e7bf..0e1a8551f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma
@@ -13,12 +13,36 @@
 (**************************************************************************)
 
 include "basic_2/reducibility/cpr_lift.ma".
+include "basic_2/reducibility/cpr_cpr.ma".
 include "basic_2/reducibility/cnf.ma".
 
 (* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
 
 (* Advanced inversion lemmas ************************************************)
 
+lemma cnf_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → L ⊢ 𝐍⦃#i⦄ → ⊥.
+#L #K #V #i #HLK #H
+elim (lift_total V 0 (i+1)) #W #HVW
+lapply (H W ?) -H [ /3 width=6/ ] -HLK #H destruct
+elim (lift_inv_lref2_be … HVW ? ?) -HVW //
+qed-.
+
+lemma cnf_inv_abst: ∀a,L,V,T. L ⊢ 𝐍⦃ⓛ{a}V.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓛV ⊢ 𝐍⦃T⦄.
+#a #L #V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+]
+qed-.
+
+lemma cnf_inv_abbr: ∀L,V,T. L ⊢ 𝐍⦃-ⓓV.T⦄ → L ⊢ 𝐍⦃V⦄ ∧ L.ⓓV ⊢ 𝐍⦃T⦄.
+#L #V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
 (* Basic_1: was only: nf2_csort_lref *)
 lemma cnf_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L  ⊢ 𝐍⦃#i⦄.
 #L #i #HLK #X #H
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.ma
index cb860ef7d..3823b4c29 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf.ma
@@ -43,7 +43,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-fact trf_inv_atom_aux: ∀I,L,T. L ⊢ 𝐑⦃T⦄ → L = ⋆ → T =  ⓪{I} → ⊥.
+fact trf_inv_atom_aux: ∀I,L,T. L ⊢ 𝐑⦃T⦄ → L = ⋆ → T = ⓪{I} → ⊥.
 #I #L #T * -L -T
 [ #L #K #V #i #HLK #H1 #H2 destruct
   lapply (ldrop_inv_atom1 … HLK) -HLK #H destruct
@@ -60,14 +60,31 @@ qed.
 lemma trf_inv_atom: ∀I. ⋆ ⊢ 𝐑⦃⓪{I}⦄ → ⊥.
 /2 width=6/ qed-.
 
-fact crf_inv_abst_aux: ∀a,L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓛ{a}W. U →
-                       L ⊢ 𝐑⦃W⦄ ∨ L.ⓛW ⊢ 𝐑⦃U⦄.
-#a #L #W #U #T * -T
+fact trf_inv_lref_aux: ∀L,T. L ⊢ 𝐑⦃T⦄ → ∀i. T = #i → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+#L #T * -L -T
+[ #L #K #V #j #HLK #i #H destruct /2 width=3/
+| #L #V #T #_ #i #H destruct
+| #L #V #T #_ #i #H destruct
+| #J #L #V #T #_ #i #H destruct
+| #a #J #L #V #T #_ #_ #i #H destruct
+| #a #J #L #V #T #_ #_ #i #H destruct
+| #a #L #V #W #T #i #H destruct
+| #a #L #V #W #T #i #H destruct
+]
+qed.
+
+lemma trf_inv_lref: ∀L,i. L ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+/2 width=3/ qed-.
+
+fact crf_inv_ib2_aux: ∀a,I,L,W,U,T. ib2 a I → L ⊢ 𝐑⦃T⦄ → T = ⓑ{a,I}W. U →
+                      L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃U⦄.
+#a #I #L #W #U #T #HI * -T
 [ #L #K #V #i #_ #H destruct
 | #L #V #T #_ #H destruct
 | #L #V #T #_ #H destruct
 | #J #L #V #T #H1 #H2 destruct
   elim H1 -H1 #H destruct
+  elim HI -HI #H destruct
 | #b #J #L #V #T #_ #HV #H destruct /2 width=1/
 | #b #J #L #V #T #_ #HT #H destruct /2 width=1/
 | #b #L #V #W #T #H destruct
@@ -75,8 +92,9 @@ fact crf_inv_abst_aux: ∀a,L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓛ{a}W. U →
 ]
 qed.
 
-lemma crf_inv_abst: ∀a,L,W,T. L ⊢ 𝐑⦃ⓛ{a}W.T⦄ → L ⊢ 𝐑⦃W⦄ ∨ L.ⓛW ⊢ 𝐑⦃T⦄.
-/2 width=4/ qed-.
+lemma crf_inv_ib2: ∀a,I,L,W,T. ib2 a I → L ⊢ 𝐑⦃ⓑ{a,I}W.T⦄ →
+                   L ⊢ 𝐑⦃W⦄ ∨ L.ⓑ{I}W ⊢ 𝐑⦃T⦄.
+/2 width=5/ qed-.
 
 fact crf_inv_appl_aux: ∀L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓐW. U →
                        ∨∨ L ⊢ 𝐑⦃W⦄ | L ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
@@ -97,4 +115,3 @@ qed.
 
 lemma crf_inv_appl: ∀L,V,T. L ⊢ 𝐑⦃ⓐV.T⦄ → ∨∨ L ⊢ 𝐑⦃V⦄ | L ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥).
 /2 width=3/ qed-.
-   
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf_append.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf_append.ma
index 7c1f83e81..f50b97e95 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf_append.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/crf_append.ma
@@ -12,34 +12,45 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/substitution/ldrop_append.ma".
 include "basic_2/reducibility/crf.ma".
 
 (* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************)
 
-(* advanced inversion lemmas ************************************************)
-(*
-lemma crf_inv_labst_last: ∀L1,T,W. L1 ⊢ 𝐑⦃T⦄ → ⇩[0, |L1|-1] L1 ≡ ⋆.ⓛW →
-                          ∀L2. ⇩[|L1|-1, 1] L1 ≡ L2 → L2 ⊢ 𝐑⦃T⦄.
+(* Advanved properties ******************************************************)
+
+lemma crf_labst_last: ∀L,T,W. L ⊢ 𝐑⦃T⦄  → ⋆.ⓛW @@ L ⊢ 𝐑⦃T⦄.
+#L #T #W #H elim H -L -T /2 width=1/
+#L #K #V #i #HLK
+lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
+lapply (ldrop_O1_append_sn_le … HLK … (⋆.ⓛW)) -HLK /2 width=2/ -Hi /2 width=3/
+qed.
+
+lemma crf_trf: ∀T,W. ⋆ ⊢ 𝐑⦃T⦄ → ⋆.ⓛW ⊢ 𝐑⦃T⦄.
+#T #W #H lapply (crf_labst_last … W H) //
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+fact crf_inv_labst_last_aux: ∀L1,T,W. L1 ⊢ 𝐑⦃T⦄  →
+                             ∀L2. L1 = ⋆.ⓛW @@ L2 → L2 ⊢ 𝐑⦃T⦄.
 #L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/
-[ #L1 #K1 #V1 #i #HLK1 #HL1 #L2 #HL12 destruct
-  lapply (ldrop_fwd_ldrop2_length … HLK1) #H
-  elim (le_to_or_lt_eq i (|L1|-1) ?) /2 width=1/ -H #Hi destruct [ -HL1 | - HL12 ]
-  [ elim (ldrop_conf_lt … HL12 … HLK1 ?) -HLK1 -HL12 // -Hi /2 width=3/
-  | lapply (ldrop_mono … HL1 … HLK1) -HL1 -HLK1 #H destruct
+[ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct
+  lapply (ldrop_fwd_ldrop2_length … HLK1)
+  >append_length >commutative_plus normalize in ⊢ (??% → ?); #H
+  elim (le_to_or_lt_eq i (|L2|) ?) /2 width=1/ -H #Hi destruct
+  [ elim (ldrop_O1_lt … Hi) #I2 #K2 #V2 #HLK2
+    lapply (ldrop_O1_inv_append1_le … HLK1 … HLK2) -HLK1 /2 width=2/ -Hi
+    normalize #H destruct /2 width=3/
+  | lapply (ldrop_O1_inv_append1_ge … HLK1 ?) -HLK1 // <minus_n_n #H
+    lapply (ldrop_inv_refl … H) -H #H destruct
   ]
-| #a #I #L1 #V #T #HI #_
-  normalize <minus_plus_m_m #IHT #HL1 #L2 #HL12
-  lapply (ldrop_fwd_ldrop2_length … HL1) #H
-  lapply (ltn_to_ltO … H) -H #H
-  @(crf_ib2_dx … HI) @IHT
-  [ @ldrop_ldrop_lt //
-  | @ldrop_skip_lt //
+| #a #I #L1 #V #T #HI #_ #IHT #L2 #H destruct /3 width=1/
 ]
 qed.
 
-
 lemma crf_inv_labst_last: ∀L,T,W. ⋆.ⓛW @@ L ⊢ 𝐑⦃T⦄  → L ⊢ 𝐑⦃T⦄.
-#L2 #T #H elim H -L2 -T
-[ #L2 #K2 #V2 #i #HLK2 #L1 #HL12
-*)
+/2 width=4/ qed-.
+
+lemma crf_inv_trf: ∀T,W. ⋆.ⓛW ⊢ 𝐑⦃T⦄  → ⋆ ⊢ 𝐑⦃T⦄.
+/2 width=4/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma
index b271a112b..ab864268f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/thnf.ma
@@ -25,7 +25,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma twhnf_inv_tshf: ∀T. 𝐇𝐍⦃T⦄ → T ≈ T.
+lemma thnf_inv_tshf: ∀T. 𝐇𝐍⦃T⦄ → T ≈ T.
 normalize /2 width=1/
 qed-.
 
@@ -52,5 +52,5 @@ lemma tpr_tshf: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2.
 ]
 qed.
 
-lemma twhnf_tshf: ∀T. T ≈ T → 𝐇𝐍⦃T⦄.
+lemma thnf_tshf: ∀T. T ≈ T → 𝐇𝐍⦃T⦄.
 /3 width=1/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
deleted file mode 100644
index 26e2d137b..000000000
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
+++ /dev/null
@@ -1,54 +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 "basic_2/reducibility/trf.ma".
-
-(* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************)
-
-definition tif: predicate term ≝ λT. 𝐑⦃T⦄ → ⊥.
-
-interpretation "context-free irreducibility (term)"
-   'NotReducible T = (tif T).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma tif_inv_abbr: ∀V,T. 𝐈⦃ⓓV.T⦄ → ⊥.
-/2 width=1/ qed-.
-
-lemma tif_inv_abst: ∀V,T. 𝐈⦃ⓛV.T⦄ → 𝐈⦃V⦄ ∧ 𝐈⦃T⦄.
-/4 width=1/ qed-.
-
-lemma tif_inv_appl: ∀V,T. 𝐈⦃ⓐV.T⦄ → ∧∧ 𝐈⦃V⦄ & 𝐈⦃T⦄ & 𝐒⦃T⦄.
-#V #T #HVT @and3_intro /3 width=1/
-generalize in match HVT; -HVT elim T -T //
-* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
-qed-.
-
-lemma tif_inv_cast: ∀V,T. 𝐈⦃ⓝV.T⦄ → ⊥.
-/2 width=1/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma tif_atom: ∀I. 𝐈⦃⓪{I}⦄.
-/2 width=4/ qed.
-
-lemma tif_abst: ∀V,T. 𝐈⦃V⦄ →  𝐈⦃T⦄ →  𝐈⦃ⓛV.T⦄.
-#V #T #HV #HT #H
-elim (trf_inv_abst … H) -H /2 width=1/
-qed.
-
-lemma tif_appl: ∀V,T. 𝐈⦃V⦄ →  𝐈⦃T⦄ →  𝐒⦃T⦄ → 𝐈⦃ⓐV.T⦄.
-#V #T #HV #HT #S #H
-elim (trf_inv_appl … H) -H /2 width=1/
-qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma
deleted file mode 100644
index b2cce435d..000000000
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma
+++ /dev/null
@@ -1,59 +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 "basic_2/reducibility/tpr.ma".
-
-(* CONTEXT-FREE NORMAL TERMS ************************************************)
-
-definition tnf: predicate term ≝ NF … tpr (eq …).
-
-interpretation
-   "context-free normality (term)"
-   'Normal T = (tnf T).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma tnf_inv_abst: ∀a,V,T. 𝐍⦃ⓛ{a}V.T⦄ → 𝐍⦃V⦄ ∧ 𝐍⦃T⦄.
-#a #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
-]
-qed-.
-
-lemma tnf_inv_appl: ∀V,T. 𝐍⦃ⓐV.T⦄ → ∧∧ 𝐍⦃V⦄ & 𝐍⦃T⦄ & 𝐒⦃T⦄.
-#V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
-| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
-  [ elim (lift_total V1 0 1) #V2 #HV12
-    lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /2 width=3/ -HV12 #H destruct
-  | lapply (H (ⓓ{a}V1.U1) ?) -H /2 width=1/ #H destruct
-]
-qed-.
-
-lemma tnf_inv_abbr: ∀V,T. 𝐍⦃+ⓓV.T⦄ → ⊥.
-#V #T #H elim (is_lift_dec T 0 1)
-[ * #U #HTU
-  lapply (H U ?) -H /2 width=3/ #H destruct
-  elim (lift_inv_pair_xy_y … HTU)
-| #HT
-  elim (tps_full (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12
-  lapply (H (+ⓓV.T2) ?) -H /2 width=3/ -HT2 #H destruct /3 width=2/
-]
-qed.
-
-lemma tnf_inv_cast: ∀V,T. 𝐍⦃ⓝV.T⦄ → ⊥.
-#V #T #H lapply (H T ?) -H /2 width=1/ #H
-@discr_tpair_xy_y //
-qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma
deleted file mode 100644
index 7b6ed1dc7..000000000
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma
+++ /dev/null
@@ -1,74 +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 "basic_2/substitution/tps_lift.ma".
-include "basic_2/reducibility/tif.ma".
-include "basic_2/reducibility/tnf.ma".
-
-(* CONTEXT-FREE NORMAL TERMS ************************************************)
-
-(* Main properties properties ***********************************************)
-
-lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 →  𝐈⦃T1⦄ → T1 = T2.
-#T1 #T2 #H elim H -T1 -T2
-[ //
-| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
-  [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_
-    >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
-  | elim (tif_inv_cast … H)
-  ]
-| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
-  elim (tif_inv_appl … H) -H #_ #_ #H
-  elim (simple_inv_bind … H)
-| * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H
-  [ -HT2 -IHV1 -IHT1 elim (tif_inv_abbr … H)
-  | <(tps_inv_refl_SO2 … HT2 ?) -HT2 //
-    elim (tif_inv_abst … H) -H #HV1 #HT1
-    >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
-  ]
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
-  elim (tif_inv_appl … H) -H #_ #_ #H
-  elim (simple_inv_bind … H)
-| #V1 #T1 #T #T2 #_ #_ #_ #H
-  elim (tif_inv_abbr … H)
-| #V1 #T1 #T2 #_ #_ #H
-  elim (tif_inv_cast … H)
-]
-qed.
-
-theorem tif_tnf: ∀T1.  𝐈⦃T1⦄ → 𝐍⦃T1⦄.
-/3 width=1/ qed.
-
-(* Note: this property is unusual *)
-lemma tnf_trf_false: ∀T1. 𝐑⦃T1⦄ → 𝐍⦃T1⦄ → ⊥.
-#T1 #H elim H -T1
-[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/
-| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
-| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/
-| #V #T #H elim (tnf_inv_abbr … H)
-| #V #T #H elim (tnf_inv_cast … H)
-| #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H
-  elim (simple_inv_bind … H)
-]
-qed.
-
-theorem tnf_tif: ∀T1. 𝐍⦃T1⦄ → 𝐈⦃T1⦄.
-/2 width=3/ qed.
-
-lemma tnf_abst: ∀V,T. 𝐍⦃V⦄ → 𝐍⦃T⦄ → 𝐍⦃ⓛV.T⦄.
-/4 width=1/ qed.
-
-lemma tnf_appl: ∀V,T. 𝐍⦃V⦄ → 𝐍⦃T⦄ → 𝐒⦃T⦄ → 𝐍⦃ⓐV.T⦄.
-/4 width=1/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
index c16669661..9ab513458 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
@@ -147,12 +147,21 @@ lemma ldrop_skip_lt: ∀L1,L2,I,V1,V2,d,e.
 #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) // /2 width=1/
 qed.
 
-lemma ldrop_O1: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
+lemma ldrop_O1_le: ∀i,L. i ≤ |L| → ∃K. ⇩[0, i] L ≡ K.
+#i @(nat_ind_plus … i) -i /2 width=2/
+#i #IHi *
+[ #H lapply (le_n_O_to_eq … H) -H >commutative_plus normalize #H destruct 
+| #L #I #V normalize #H
+  elim (IHi L ?) -IHi /2 width=1/ -H /3 width=2/
+]
+qed.
+
+lemma ldrop_O1_lt: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
 #L elim L -L
 [ #i #H elim (lt_zero_false … H)
-| #L #I #V #IHL #i @(nat_ind_plus … i) -i /2 width=4/ #i #_ #H
-  lapply (lt_plus_to_lt_l … H) -H #Hi
-  elim (IHL i ?) // /3 width=4/
+| #L #I #V #IHL #i @(nat_ind_plus … i) -i /2 width=4/
+  #i #_ normalize #H
+  elim (IHL i ? ) -IHL /2 width=1/ -H /3 width=4/
 ]
 qed.
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma
index ec5258552..3f6b2c538 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma
@@ -19,8 +19,20 @@ include "basic_2/substitution/ldrop.ma".
 
 (* Properties on append for local environments ******************************)
 
-lemma ldrop_append_O1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
-                          |L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.
+fact ldrop_O1_append_sn_le_aux: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → 
+                                d = 0 → e ≤ |L1| →
+                                ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize // /4 width=1/
+#d #e #_ #H #L -d
+lapply (le_n_O_to_eq … H) -H //
+qed-.
+
+lemma ldrop_O1_append_sn_le: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → e ≤ |L1| →
+                             ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
+/2 width=3 by ldrop_O1_append_sn_le_aux/ qed.
+
+lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
+                               |L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.
 #K #L1 #L2 elim L2 -L2 normalize //
 #L2 #I #V #IHL2 #e #H #H1e
 elim (ldrop_inv_O1 … H) -H * #H2e #HL12 destruct
@@ -28,16 +40,22 @@ elim (ldrop_inv_O1 … H) -H * #H2e #HL12 destruct
   >commutative_plus normalize #H destruct
 | <minus_plus >minus_minus_comm /3 width=1/
 ]
-qed.
+qed-.
 
-lemma ldrop_append_O1_lt: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e < |L2| →
-                          ∃∃K2. ⇩[0, e] L2 ≡ K2 & K = L1 @@ K2.
-#K #L1 #L2 elim L2 -L2
-[ #e #_ #H elim (lt_zero_false … H)
-| #L2 #I #V #IHL2 #e normalize #HL12 #H1e
-  elim (ldrop_inv_O1 … HL12) -HL12 * #H2e #HL12 destruct
-  [ -H1e -IHL2 /3 width=3/
-  | elim (IHL2 … HL12 ?) -IHL2 -HL12 /2 width=1/ -H1e #K2 #HLK2 #H destruct /3 width=3/
+lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e ≤ |L2| →
+                               ∀K2. ⇩[0, e] L2 ≡ K2 → K = L1 @@ K2.
+#K #L1 #L2 elim L2 -L2 normalize
+[ #e #H1 #H2 #K2 #H3
+  lapply (le_n_O_to_eq … H2) -H2 #H2
+  lapply (ldrop_inv_atom1 … H3) -H3 #H3 destruct
+  >(ldrop_inv_refl … H1) -H1 //
+| #L2 #I #V #IHL2 #e @(nat_ind_plus … e) -e [ -IHL2 ]
+  [ #H1 #_ #K2 #H2
+    lapply (ldrop_inv_refl … H1) -H1 #H1
+    lapply (ldrop_inv_refl … H2) -H2 #H2 destruct //
+  | #e #_ #H1 #H1e #K2 #H2
+    lapply (ldrop_inv_ldrop1 … H1 ?) -H1 //
+    lapply (ldrop_inv_ldrop1 … H2 ?) -H2 // /3 width=4/
   ]
 ]
-qed.
+qed-. 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
index 26c4e3e8a..a53033aa0 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
@@ -37,7 +37,7 @@ fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 
   elim (lt_or_ge i d) #Hdi [ /3 width=2/ ]
   elim (lt_or_ge i (d+e)) #Hide [2: /3 width=2/ ]
   lapply (lt_to_le_to_lt … Hide Hde) #Hi
-  elim (ldrop_O1 … Hi) -Hi #I #K #V1 #HLK
+  elim (ldrop_O1_lt … Hi) -Hi #I #K #V1 #HLK
   lapply (sfr_inv_ldrop … HLK … HL ? ?) // #H destruct
   lapply (ldrop_pair2_fwd_cw … HLK (#i)) #HKL
   lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml
index 2d7b981c1..c150f4503 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml
@@ -39,5 +39,6 @@
     <key name="or">3</key>
     <key name="or">4</key>
     <key name="and">3</key>
+    <key name="and">4</key>
   </section>
 </helm_registry>
diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
index 3d265bc47..f4296024f 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
@@ -221,3 +221,11 @@ inductive and3 (P0,P1,P2:Prop) : Prop ≝
 
 interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2).
 
+(* multiple conjunction connective (4) *)
+
+inductive and4 (P0,P1,P2,P3:Prop) : Prop ≝
+   | and4_intro: P0 → P1 → P2 → P3 → and4 ? ? ? ?
+.
+
+interpretation "multiple conjunction connective (4)" 'And P0 P1 P2 P3 = (and4 P0 P1 P2 P3).
+
diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma
index 8a167c86a..ed4b83f83 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma
@@ -252,3 +252,9 @@ notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2)"
  non associative with precedence 35
  for @{ 'And $P0 $P1 $P2 }.
 
+(* multiple conjunction connective (4) *)
+
+notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2 break & term 34 P3)"
+ non associative with precedence 35
+ for @{ 'And $P0 $P1 $P2 $P3 }.
+
diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml
index d32f69cf0..2bbe85225 100644
--- a/matita/matita/matita.ml
+++ b/matita/matita/matita.ml
@@ -37,7 +37,8 @@ let _ =
     ["-tptppath",Arg.String 
       (fun s -> Helm_registry.set_string "matita.tptppath" s),
       "Where to find the Axioms/ and Problems/ directory"];
-  MatitaInit.initialize_all ()
+  MatitaInit.initialize_all ();
+  MatitaMisc.reset_font_size ()
 ;;
 
 let _ =
-- 
2.39.2