partial update in static_2

+ propagation of ground library in static_2/relocation begins
+ additions in ground

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma
index f25cd9b512f3b5de781fe02b5b4638992622e9f2..2128885217bc56f8596871d7caf95527197613d6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "ground/relocation/pr_pat_lt.ma".
+include "ground/relocation/pr_nat.ma".
 include "ground/relocation/pr_ist.ma".
 include "ground/relocation/pr_after_pat.ma".
 
@@ -52,6 +53,14 @@ lemma pr_after_des_ist_pat:
 /3 width=8 by pr_after_des_pat, ex2_intro/
 qed-.
 
+lemma pr_after_des_ist_nat:
+      ∀f1,l1,l2. @↑❪l1, f1❫ ≘ l2 → ∀f2. 𝐓❪f2❫ → ∀f. f2 ⊚ f1 ≘ f →
+      ∃∃l. @↑❪l2, f2❫ ≘ l & @↑❪l1, f❫ ≘ l.
+#f1 #l1 #l2 #H1 #f2 #H2 #f #Hf
+elim (pr_after_des_ist_pat … H1 … H2 … Hf) -f1 -H2
+/2 width=3 by ex2_intro/
+qed-.
+
 (* Inversions with pr_ist ***************************************************)
 
 (*** after_inv_istot *)

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat.ma
new file mode 100644 (file)
index 0000000..238a911
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/pr_nat.ma".
+include "ground/relocation/pr_after_pat.ma".
+
+(* RELATIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************)
+
+(* Destructions with pr_nat *************************************************)
+
+lemma pr_after_nat_des (l) (l1):
+      ∀f. @↑❪l1, f❫ ≘ l → ∀f2,f1. f2 ⊚ f1 ≘ f →
+      ∃∃l2. @↑❪l1, f1❫ ≘ l2 & @↑❪l2, f2❫ ≘ l.
+#l #l1 #f #H1 #f2 #f1 #Hf
+elim (pr_after_pat_des … H1 … Hf) -f #i2 #H1 #H2
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma pr_after_des_nat (l) (l2) (l1):
+      ∀f1,f2. @↑❪l1, f1❫ ≘ l2 → @↑❪l2, f2❫ ≘ l →
+      ∀f. f2 ⊚ f1 ≘ f → @↑❪l1, f❫ ≘ l.
+/2 width=6 by pr_after_des_pat/ qed-.
+
+lemma pr_after_des_nat_sn (l1) (l):
+      ∀f. @↑❪l1, f❫ ≘ l → ∀f1,l2. @↑❪l1, f1❫ ≘ l2 →
+      ∀f2. f2 ⊚ f1 ≘ f → @↑❪l2, f2❫ ≘ l.
+/2 width=6 by pr_after_des_pat_sn/ qed-.
+
+lemma pr_after_des_nat_dx (l) (l2) (l1):
+      ∀f,f2. @↑❪l1, f❫ ≘ l → @↑❪l2, f2❫ ≘ l →
+      ∀f1. f2 ⊚ f1 ≘ f → @↑❪l1, f1❫ ≘ l2.
+/2 width=6 by pr_after_des_pat_dx/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
index 0629472e2f285e126f48da111e62ca4d66470066..4cd185f2a692c566e4b16001eee76119a474fe59 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/relocation/pr_after.ma".
+include "ground/relocation/pr_after_after.ma".
 
-(* RELATIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************)
+(* FUNCTIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************)
 
 corec definition pr_compose: pr_map → pr_map → pr_map.
 * * #g2 [ #f1 | * * #g1 ]
@@ -40,6 +40,7 @@ lemma pr_compose_unfold_push (f2) (f1): ↑(f2∘f1) = (⫯f2)∘(↑f1).
 <(stream_unfold … ((⫯f2)∘(↑f1))) in ⊢ (???%); //
 qed.
 
+(*** compose_next *)
 lemma pr_compose_unfold_next (f2) (f1):
       ↑(f2∘f1) = (↑f2)∘f1.
 #f2 #f1
@@ -48,7 +49,8 @@ qed.
 
 (* Main constructions *******************************************************)
 
-corec theorem pr_after_compose (f2) (f1):
+(*** after_total *)
+corec theorem pr_after_total (f2) (f1):
               f2 ⊚ f1 ≘ f2∘f1.
 cases (pr_map_split_tl f2)*
 [ cases (pr_map_split_tl f1) * ]
@@ -57,3 +59,9 @@ cases (pr_map_split_tl f2)*
 | @pr_after_next /2 width=5 by/
 ]
 qed.
+
+(* Main inversions **********************************************************)
+
+(*** after_inv_total *)
+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_isi_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_nat.ma
new file mode 100644 (file)
index 0000000..6552826
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_nat.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/pr_nat.ma".
+include "ground/relocation/pr_isi_pat.ma".
+
+(* IDENTITY CONDITION FOR PARTIAL RELOCATION MAPS ***************************)
+
+(* Advanced constructions with pr_isi and pr_nat ****************************)
+
+lemma pr_isi_nat (f): (∀l. @↑❪l,f❫ ≘ l) → 𝐈❪f❫.
+/2 width=1 by pr_isi_pat/ qed.
+
+(* Inversions with pr_nat ***************************************************)
+
+lemma pr_isi_inv_nat (f) (l): 𝐈❪f❫ → @↑❪l,f❫ ≘ l.
+/2 width=1 by pr_isi_inv_pat/ qed-.
+
+(* Destructions with pr_nat *************************************************)
+
+lemma pr_isi_nat_des (f) (l1) (l2): 𝐈❪f❫ → @↑❪l1,f❫ ≘ l2 → l1 = l2.
+/3 width=3 by pr_isi_pat_des, eq_inv_npsucc_bi/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma
index 7ee376ea1b0e554d29904d45275ddd4ceb5ff95b..9d4997f10777e01ae8d3e053e0bbdcae593830d1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma
@@ -17,7 +17,7 @@ include "ground/relocation/pr_pat_pat_id.ma".
 
 (* IDENTITY CONDITION FOR PARTIAL RELOCATION MAPS ***************************)
 
-(* Advanced constructions with pr_isi ***************************************)
+(* Advanced constructions with pr_isi and pr_pat ****************************)
 
 (*** isid_at *)
 lemma pr_isi_pat (f): (∀i. @❪i,f❫ ≘ i) → 𝐈❪f❫.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma
index c1ab3435e85a18ec94898cf9a0fc0b30d58d5ec1..607a16e974ceb3ef0aa5d0dd7b9534708d2e0ab2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma
@@ -39,6 +39,20 @@ lemma pr_ist_inv_next (g): 𝐓❪g❫ → ∀f. ↑f = g → 𝐓❪f❫.
 #j #Hg elim (pr_pat_inv_next … Hg … H) -Hg -H /2 width=2 by ex_intro/
 qed-.
 
+(* Basic constructions ******************************************************)
+
+lemma pr_ist_push (f): 𝐓❪f❫ → 𝐓❪⫯f❫.
+#f #Hf *
+[ /3 width=2 by pr_pat_refl, ex_intro/
+| #i elim (Hf i) -Hf /3 width=8 by pr_pat_push, ex_intro/
+]
+qed.
+
+lemma pr_ist_next (f): 𝐓❪f❫ → 𝐓❪↑f❫.
+#f #Hf #i elim (Hf i) -Hf
+/3 width=6 by pr_pat_next, ex_intro/
+qed.
+
 (* Constructions with pr_tl *************************************************)
 
 (*** istot_tl *)

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 1d76991d1dc3d5af74e15cb6f6894977304e98a9..0b4a769f84859c0381e4516d5533ba21836d27ab 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
@@ -15,6 +15,7 @@
 include "ground/relocation/pr_eq.ma".
 include "ground/relocation/pr_pat_lt.ma".
 include "ground/relocation/pr_pat_pat.ma".
+include "ground/relocation/pr_nat.ma".
 include "ground/relocation/pr_ist.ma".
 
 (* TOTALITY CONDITION FOR PARTIAL RELOCATION MAPS ***************************)
@@ -66,3 +67,12 @@ cases (pr_map_split_tl f2) #H2
   lapply (Hi i (↑i1) (↑i2) ??) /2 width=5 by pr_pat_next/
 ]
 qed-.
+
+(* Advanced constructions with pr_nat ***************************************)
+
+lemma is_pr_nat_dec (f) (l2): 𝐓❪f❫ → Decidable (∃l1. @↑❪l1,f❫ ≘ l2).
+#f #l2 #Hf elim (is_pr_pat_dec … (↑l2) Hf)
+[ * /3 width=2 by ex_intro, or_introl/
+| #H @or_intror * /3 width=2 by ex_intro/
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index a84e3e1a38b41a9491c11edba24a975c468ba854..da49c6c4831c8f514b668e50d88e34bfd60d060a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -35,13 +35,13 @@ table {
           [ "pr_sdj ( ? ∥ ? )" "pr_sdj_eq" "pr_sdj_isi" * ]
           [ "pr_sle ( ? ⊆ ? )" "pr_sle_eq" "pr_sle_pushs" "pr_sle_tls" "pr_sle_isi" "pr_sle_isd" "pr_sle_sle" * ]
           [ "pr_coafter ( ? ~⊚ ? ≘ ? )" "pr_coafter_eq" "pr_coafter_uni_pushs" "pr_coafter_pat_tls" "pr_coafter_nat_tls" "pr_coafter_nat_tls_pushs" "pr_coafter_isi" "pr_coafter_isu" "pr_coafter_ist_isi" "pr_coafter_ist_isf" "pr_coafter_coafter" "pr_coafter_coafter_ist" * ]
-          [ "pr_after ( ? ⊚ ? ≘ ? )" "pr_after_eq" "pr_after_uni" "pr_after_basic" "pr_after_pat" "pr_after_pat_tls" "pr_after_pat_uni_tls" "pr_after_nat_uni_tls" "pr_after_isi" "pr_after_isu" "pr_after_ist" "pr_after_ist_isi" "pr_after_after" "pr_after_after_ist" * ]
+          [ "pr_after ( ? ⊚ ? ≘ ? )" "pr_after_eq" "pr_after_uni" "pr_after_basic" "pr_after_pat" "pr_after_pat_tls" "pr_after_pat_uni_tls" "pr_after_nat" "pr_after_nat_uni_tls" "pr_after_isi" "pr_after_isu" "pr_after_ist" "pr_after_ist_isi" "pr_after_after" "pr_after_after_ist" * ]
           [ "pr_isd ( 𝛀❪?❫ )" "pr_isd_eq" "pr_isd_tl" "pr_isd_nexts" "pr_isd_tls" * ]
           [ "pr_ist ( 𝐓❪?❫ )" "pr_ist_tls" "pr_ist_isi" "pr_ist_ist" * ]
           [ "pr_isf ( 𝐅❪?❫ )" "pr_isf_eq" "pr_isf_tl" "pr_isf_pushs" "fr_isf_tls" "pr_ifs_uni" "pr_isf_isu" * ]
           [ "pr_fcla ( 𝐂❪?❫ ≘ ? )" "pr_fcla_eq" "fcla_uni" "pr_fcla_fcla" * ]
           [ "pr_isu ( 𝐔❪?❫ )" "pr_isu_tl" "pr_isu_uni" * ]
-          [ "pr_isi ( 𝐈❪?❫ )" "pr_isi_eq" "pr_isi_tl" "pr_isi_pushs" "pr_isi_tls" "pr_isi_id" "pr_isi_uni" "pr_isi_pat" * ]
+          [ "pr_isi ( 𝐈❪?❫ )" "pr_isi_eq" "pr_isi_tl" "pr_isi_pushs" "pr_isi_tls" "pr_isi_id" "pr_isi_uni" "pr_isi_pat" "pr_isi_nat" * ]
           [ "pr_nat ( @↑❪?,?❫ ≘ ? )" "pr_nat_uni" "pr_nat_basic" "pr_nat_nat" * ]
           [ "pr_pat ( @❪?,?❫ ≘ ? )" "pr_pat_lt" "pr_pat_eq" "pr_pat_tls" "pr_pat_id" "pr_pat_uni" "pr_pat_basic" "pr_pat_pat" "pr_pat_pat_id" * ]
           [ "pr_basic ( 𝐛❨?,?❩ )" * ]

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
index f019c66d6cb3fa61170a17457061e3f2d375a13f..e88d128d37c256f854d1da87af926fbdb2aa4c32 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
@@ -12,7 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/relocation/nstream_after.ma".
+include "ground/arith/nat_le_plus.ma".
+include "ground/relocation/pr_compose.ma".
+include "ground/relocation/pr_nat_uni.ma".
+include "ground/relocation/pr_isi_nat.ma".
+include "ground/relocation/pr_ist_ist.ma".
+include "ground/relocation/pr_after_uni.ma".
+include "ground/relocation/pr_after_nat.ma".
+include "ground/relocation/pr_after_ist.ma".
 include "static_2/notation/relations/rliftstar_3.ma".
 include "static_2/notation/relations/rlift_3.ma".
 include "static_2/syntax/term.ma".
@@ -25,7 +32,7 @@ include "static_2/syntax/term.ma".
 *)
 inductive lifts: pr_map → relation term ≝
 | lifts_sort: ∀f,s. lifts f (⋆s) (⋆s)
-| lifts_lref: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → lifts f (#i1) (#i2)
+| lifts_lref: â\88\80f,i1,i2. @â\86\91â\9dªi1,fâ\9d« â\89\98 i2 â\86\92 lifts f (#i1) (#i2)
 | lifts_gref: ∀f,l. lifts f (§l) (§l)
 | lifts_bind: ∀f,p,I,V1,V2,T1,T2.
               lifts f V1 V2 → lifts (⫯f) T1 T2 →
@@ -81,7 +88,7 @@ lemma lifts_inv_sort1: ∀f,Y,s. ⇧*[f] ⋆s ≘ Y → Y = ⋆s.
 /2 width=4 by lifts_inv_sort1_aux/ qed-.
 
 fact lifts_inv_lref1_aux: ∀f,X,Y. ⇧*[f] X ≘ Y → ∀i1. X = #i1 →
-                          ∃∃i2. @❪i1,f❫ ≘ i2 & Y = #i2.
+                          â\88\83â\88\83i2. @â\86\91â\9dªi1,fâ\9d« â\89\98 i2 & Y = #i2.
 #f #X #Y * -f -X -Y
 [ #f #s #x #H destruct
 | #f #i1 #i2 #Hi12 #x #H destruct /2 width=3 by ex2_intro/
@@ -94,7 +101,7 @@ qed-.
 (* Basic_1: was: lift1_lref *)
 (* Basic_2A1: includes: lift_inv_lref1 lift_inv_lref1_lt lift_inv_lref1_ge *)
 lemma lifts_inv_lref1: ∀f,Y,i1. ⇧*[f] #i1 ≘ Y →
-                       ∃∃i2. @❪i1,f❫ ≘ i2 & Y = #i2.
+                       â\88\83â\88\83i2. @â\86\91â\9dªi1,fâ\9d« â\89\98 i2 & Y = #i2.
 /2 width=3 by lifts_inv_lref1_aux/ qed-.
 
 fact lifts_inv_gref1_aux: ∀f,X,Y. ⇧*[f] X ≘ Y → ∀l. X = §l → Y = §l.
@@ -163,7 +170,7 @@ lemma lifts_inv_sort2: ∀f,X,s. ⇧*[f] X ≘ ⋆s → X = ⋆s.
 /2 width=4 by lifts_inv_sort2_aux/ qed-.
 
 fact lifts_inv_lref2_aux: ∀f,X,Y. ⇧*[f] X ≘ Y → ∀i2. Y = #i2 →
-                          ∃∃i1. @❪i1,f❫ ≘ i2 & X = #i1.
+                          â\88\83â\88\83i1. @â\86\91â\9dªi1,fâ\9d« â\89\98 i2 & X = #i1.
 #f #X #Y * -f -X -Y
 [ #f #s #x #H destruct
 | #f #i1 #i2 #Hi12 #x #H destruct /2 width=3 by ex2_intro/
@@ -176,7 +183,7 @@ qed-.
 (* Basic_1: includes: lift_gen_lref lift_gen_lref_lt lift_gen_lref_false lift_gen_lref_ge *)
 (* Basic_2A1: includes: lift_inv_lref2 lift_inv_lref2_lt lift_inv_lref2_be lift_inv_lref2_ge lift_inv_lref2_plus *)
 lemma lifts_inv_lref2: ∀f,X,i2. ⇧*[f] X ≘ #i2 →
-                       ∃∃i1. @❪i1,f❫ ≘ i2 & X = #i1.
+                       â\88\83â\88\83i1. @â\86\91â\9dªi1,fâ\9d« â\89\98 i2 & X = #i1.
 /2 width=3 by lifts_inv_lref2_aux/ qed-.
 
 fact lifts_inv_gref2_aux: ∀f,X,Y. ⇧*[f] X ≘ Y → ∀l. Y = §l → X = §l.
@@ -235,7 +242,7 @@ lemma lifts_inv_flat2: ∀f,I,V2,T2,X. ⇧*[f] X ≘ ⓕ[I]V2.T2 →
 
 lemma lifts_inv_atom1: ∀f,I,Y. ⇧*[f] ⓪[I] ≘ Y →
                        ∨∨ ∃∃s. I = Sort s & Y = ⋆s
-                        | ∃∃i,j. @❪i,f❫ ≘ j & I = LRef i & Y = #j
+                        | â\88\83â\88\83i,j. @â\86\91â\9dªi,fâ\9d« â\89\98 j & I = LRef i & Y = #j
                         | ∃∃l. I = GRef l & Y = §l.
 #f * #n #Y #H
 [ lapply (lifts_inv_sort1 … H)
@@ -246,7 +253,7 @@ qed-.
 
 lemma lifts_inv_atom2: ∀f,I,X. ⇧*[f] X ≘ ⓪[I] →
                        ∨∨ ∃∃s. X = ⋆s & I = Sort s
-                        | ∃∃i,j. @❪i,f❫ ≘ j & X = #i & I = LRef j
+                        | â\88\83â\88\83i,j. @â\86\91â\9dªi,fâ\9d« â\89\98 j & X = #i & I = LRef j
                         | ∃∃l. X = §l & I = GRef l.
 #f * #n #X #H
 [ lapply (lifts_inv_sort2 … H)
@@ -289,7 +296,7 @@ lemma lifts_inv_pair_xy_y: ∀I,T,V,f. ⇧*[f] ②[I]V.T ≘ T → ⊥.
 qed-.
 
 lemma lifts_inv_push_zero_sn (f):
-      ∀X. ⇧*[⫯f]#0 ≘ X → #0 = X.
+      ∀X. ⇧*[⫯f]#𝟎 ≘ X → #(𝟎) = X.
 #f #X #H
 elim (lifts_inv_lref1 … H) -H #i #Hi #H destruct
 lapply (pr_pat_inv_unit_push … Hi ???) -Hi //
@@ -300,30 +307,34 @@ lemma lifts_inv_push_succ_sn (f) (i1):
       ∃∃i2. ⇧*[f]#i1 ≘ #i2 & #(↑i2) = X.
 #f #i1 #X #H
 elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct
-elim (pr_pat_inv_succ_push … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct
+elim (pr_nat_inv_succ_push … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct
 /3 width=3 by lifts_lref, ex2_intro/
 qed-.
 
 (* Inversion lemmas with uniform relocations ********************************)
 
 lemma lifts_inv_lref1_uni: ∀l,Y,i. ⇧[l] #i ≘ Y → Y = #(l+i).
-#l #Y #i1 #H elim (lifts_inv_lref1 … H) -H /4 width=4 by fr2_nat_mono, eq_f/
+#l #Y #i1 #H elim (lifts_inv_lref1 … H) -H
+#i2 #H #H2 destruct
+/4 width=4 by pr_nat_mono, eq_f/
 qed-.
 
 lemma lifts_inv_lref2_uni: ∀l,X,i2. ⇧[l] X ≘ #i2 →
-                           ∃∃i1. X = #i1 & i2 = l + i1.
+                           ∃∃i1. X = #i1 & i1 + l = i2.
 #l #X #i2 #H elim (lifts_inv_lref2 … H) -H
-/3 width=3 by pr_pat_inv_uni, ex2_intro/
+/3 width=3 by pr_nat_inv_uni, ex2_intro/
 qed-.
 
-lemma lifts_inv_lref2_uni_ge: ∀l,X,i. ⇧[l] X ≘ #(l + i) → X = #i.
+lemma lifts_inv_lref2_uni_ge: ∀l,X,i. ⇧[l] X ≘ #(i+l) → X = #i.
 #l #X #i2 #H elim (lifts_inv_lref2_uni … H) -H
-#i1 #H1 #H2 destruct /4 width=2 by eq_inv_nplus_bi_sn, eq_f, sym_eq/
+#i1 #H1 #H2 destruct
+/4 width=2 by eq_inv_nplus_bi_dx, eq_f/
 qed-.
 
 lemma lifts_inv_lref2_uni_lt: ∀l,X,i. ⇧[l] X ≘ #i → i < l → ⊥.
 #l #X #i2 #H elim (lifts_inv_lref2_uni … H) -H
-#i1 #_ #H1 #H2 destruct /2 width=4 by nlt_ge_false/
+#i1 #_ #H1 #H2 destruct
+/2 width=4 by nlt_ge_false/
 qed-.
 
 (* Basic forward lemmas *****************************************************)
@@ -331,7 +342,7 @@ qed-.
 (* Basic_2A1: includes: lift_inv_O2 *)
 lemma lifts_fwd_isid: ∀f,T1,T2. ⇧*[f] T1 ≘ T2 → 𝐈❪f❫ → T1 = T2.
 #f #T1 #T2 #H elim H -f -T1 -T2
-/4 width=3 by pr_isi_pat_des, pr_isi_push, eq_f2, eq_f/
+/4 width=3 by pr_isi_nat_des, pr_isi_push, eq_f2, eq_f/
 qed-.
 
 (* Basic_2A1: includes: lift_fwd_pair1 *)
@@ -381,18 +392,19 @@ lemma lifts_refl: ∀T,f. 𝐈❪f❫ → ⇧*[f] T ≘ T.
 qed.
 
 (* Basic_2A1: includes: lift_total *)
-lemma lifts_total: ∀T1,f. ∃T2. ⇧*[f] T1 ≘ T2.
+lemma lifts_total: ∀T1,f. 𝐓❪f❫ → ∃T2. ⇧*[f] T1 ≘ T2.
 #T1 elim T1 -T1 *
-/3 width=2 by lifts_lref, lifts_sort, lifts_gref, ex_intro/
-[ #p ] #I #V1 #T1 #IHV1 #IHT1 #f
-elim (IHV1 f) -IHV1 #V2 #HV12
-[ elim (IHT1 (⫯f)) -IHT1 /3 width=2 by lifts_bind, ex_intro/
+/3 width=2 by lifts_sort, lifts_gref, ex_intro/
+[ #i #f #Hf elim (Hf (↑i)) -Hf /3 width=2 by ex_intro, lifts_lref/ ]
+[ #p ] #I #V1 #T1 #IHV1 #IHT1 #f #Hf
+elim (IHV1 f) -IHV1 // #V2 #HV12
+[ elim (IHT1 (⫯f)) -IHT1 /3 width=2 by pr_ist_push, ex_intro, lifts_bind/
 | elim (IHT1 f) -IHT1 /3 width=2 by lifts_flat, ex_intro/
 ]
 qed-.
 
-lemma lifts_push_zero (f): ⇧*[⫯f]#0 ≘ #0.
-/2 width=1 by lifts_lref/ qed.
+lemma lifts_push_zero (f): ⇧*[⫯f]#(𝟎) ≘ #(𝟎).
+/3 width=2 by pr_nat_refl, lifts_lref/ qed.
 
 lemma lifts_push_lref (f) (i1) (i2): ⇧*[f]#i1 ≘ #i2 → ⇧*[⫯f]#(↑i1) ≘ #(↑i2).
 #f1 #i1 #i2 #H
@@ -411,12 +423,12 @@ lemma lifts_split_trans: ∀f,T1,T2. ⇧*[f] T1 ≘ T2 →
                          ∃∃T. ⇧*[f1] T1 ≘ T & ⇧*[f2] T ≘ T2.
 #f #T1 #T2 #H elim H -f -T1 -T2
 [ /3 width=3 by lifts_sort, ex2_intro/
-| #f #i1 #i2 #Hi #f1 #f2 #Ht elim (pr_after_pat_des … Hi … Ht) -Hi -Ht
+| #f #i1 #i2 #Hi #f1 #f2 #Ht elim (pr_after_nat_des … Hi … Ht) -Hi -Ht
   /3 width=3 by lifts_lref, ex2_intro/
 | /3 width=3 by lifts_gref, ex2_intro/
 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f1 #f2 #Ht
   elim (IHV … Ht) elim (IHT (⫯f1) (⫯f2)) -IHV -IHT
-  /3 width=5 by lifts_bind, after_O2, ex2_intro/
+  /3 width=7 by pr_after_refl, ex2_intro, lifts_bind/
 | #f #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f1 #f2 #Ht
   elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht
   /3 width=5 by lifts_flat, ex2_intro/
@@ -425,17 +437,18 @@ qed-.
 
 (* Note: apparently, this was missing in Basic_2A1 *)
 lemma lifts_split_div: ∀f1,T1,T2. ⇧*[f1] T1 ≘ T2 →
-                       ∀f2,f. f2 ⊚ f1 ≘ f →
+                       ∀f2. 𝐓❪f2❫ → ∀f. f2 ⊚ f1 ≘ f →
                        ∃∃T. ⇧*[f2] T2 ≘ T & ⇧*[f] T1 ≘ T.
 #f1 #T1 #T2 #H elim H -f1 -T1 -T2
 [ /3 width=3 by lifts_sort, ex2_intro/
-| #f1 #i1 #i2 #Hi #f2 #f #Ht elim (pr_after_des_ist_pat … Hi … Ht) -Hi -Ht
+| #f1 #i1 #i2 #Hi #f2 #Hf2 #f #Ht
+  elim (pr_after_des_ist_nat … Hi … Ht) -Hi -Ht
   /3 width=3 by lifts_lref, ex2_intro/
 | /3 width=3 by lifts_gref, ex2_intro/
-| #f1 #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #f #Ht
-  elim (IHV … Ht) elim (IHT (⫯f2) (⫯f)) -IHV -IHT
-  /3 width=5 by lifts_bind, after_O2, ex2_intro/
-| #f1 #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #f #Ht
+| #f1 #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #Hf2 #f #Ht
+  elim (IHV … Ht) elim (IHT (⫯f2) … (⫯f)) -IHV -IHT
+  /3 width=7 by pr_ist_push, pr_after_refl, ex2_intro, lifts_bind/
+| #f1 #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #Hf2 #f #Ht
   elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht
   /3 width=5 by lifts_flat, ex2_intro/
 ]
@@ -443,18 +456,18 @@ qed-.
 
 (* Basic_1: includes: dnf_dec2 dnf_dec *)
 (* Basic_2A1: includes: is_lift_dec *)
-lemma is_lifts_dec: ∀T2,f. Decidable (∃T1. ⇧*[f] T1 ≘ T2).
+lemma is_lifts_dec: ∀T2,f. 𝐓❪f❫ → Decidable (∃T1. ⇧*[f] T1 ≘ T2).
 #T1 elim T1 -T1
 [ * [1,3: /3 width=2 by lifts_sort, lifts_gref, ex_intro, or_introl/ ]
-  #i2 #f elim (is_pr_pat_dec f i2) //
+  #i2 #f #Hf elim (is_pr_nat_dec f i2) //
   [ * /4 width=3 by lifts_lref, ex_intro, or_introl/
   | #H @or_intror *
     #X #HX elim (lifts_inv_lref2 … HX) -HX
     /3 width=2 by ex_intro/
   ]
-| * [ #p ] #I #V2 #T2 #IHV2 #IHT2 #f
-  [ elim (IHV2 f) -IHV2
-    [ * #V1 #HV12 elim (IHT2 (⫯f)) -IHT2
+| * [ #p ] #I #V2 #T2 #IHV2 #IHT2 #f #Hf
+  [ elim (IHV2 f) -IHV2 //
+    [ * #V1 #HV12 elim (IHT2 (⫯f)) -IHT2 /2 width=1 by pr_ist_push/
       [ * #T1 #HT12 @or_introl /3 width=2 by lifts_bind, ex_intro/
       | -V1 #HT2 @or_intror * #X #H
         elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/
@@ -462,8 +475,8 @@ lemma is_lifts_dec: ∀T2,f. Decidable (∃T1. ⇧*[f] T1 ≘ T2).
     | -IHT2 #HV2 @or_intror * #X #H
       elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/
     ]
-  | elim (IHV2 f) -IHV2
-    [ * #V1 #HV12 elim (IHT2 f) -IHT2
+  | elim (IHV2 f) -IHV2 //
+    [ * #V1 #HV12 elim (IHT2 f) -IHT2 //
       [ * #T1 #HT12 /4 width=2 by lifts_flat, ex_intro, or_introl/
       | -V1 #HT2 @or_intror * #X #H
         elim (lifts_inv_flat2 … H) -H /3 width=2 by ex_intro/
@@ -477,8 +490,8 @@ qed-.
 
 (* Properties with uniform relocation ***************************************)
 
-lemma lifts_uni: â\88\80n1,n2,T,U. â\87§*[ð\9d\90\94â\9d¨n1â\9d©â\88\98ð\9d\90\94â\9d¨n2❩] T ≘ U → ⇧[n1+n2] T ≘ U.
-/3 width=4 by lifts_eq_repl_back, after_inv_total/ qed.
+lemma lifts_uni: â\88\80n1,n2,T,U. â\87§*[ð\9d\90®â\9d¨n2â\9d©â\88\98ð\9d\90®â\9d¨n1❩] T ≘ U → ⇧[n1+n2] T ≘ U.
+/3 width=4 by lifts_eq_repl_back, pr_after_inv_total/ qed.
 
 (* Basic_2A1: removed theorems 14:
               lifts_inv_nil lifts_inv_cons