matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "ground/xoa/ex_1_2.ma".
  16 include "ground/xoa/ex_4_3.ma".
  17 include "ground/relocation/rtmap_coafter.ma".
  18 include "static_2/notation/relations/rdropstar_4.ma".
  19 include "static_2/notation/relations/rdrop_3.ma".
  20 include "static_2/relocation/seq.ma".
  21 include "static_2/relocation/lifts_bind.ma".
  22
  23 (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
  24
  25 (* Basic_1: includes: drop_skip_bind drop1_skip_bind *)
  26 (* Basic_2A1: includes: drop_atom drop_pair drop_drop drop_skip
  27                         drop_refl_atom_O2 drop_drop_lt drop_skip_lt
  28 *)
  29 inductive drops (b:bool): rtmap → relation lenv ≝
  30 | drops_atom: ∀f. (b = Ⓣ → 𝐈❪f❫) → drops b (f) (⋆) (⋆)
  31 | drops_drop: ∀f,I,L1,L2. drops b f L1 L2 → drops b (↑f) (L1.ⓘ[I]) L2
  32 | drops_skip: ∀f,I1,I2,L1,L2.
  33               drops b f L1 L2 → ⇧*[f] I2 ≘ I1 →
  34               drops b (⫯f) (L1.ⓘ[I1]) (L2.ⓘ[I2])
  35 .
  36
  37 interpretation "generic slicing (local environment)"
  38    'RDropStar b f L1 L2 = (drops b f L1 L2).
  39
  40 interpretation "uniform slicing (local environment)"
  41    'RDrop i L1 L2 = (drops true (uni i) L1 L2).
  42
  43 definition d_liftable1: predicate (relation2 lenv term) ≝
  44                         λR. ∀K,T. R K T → ∀b,f,L. ⇩*[b,f] L ≘ K →
  45                         ∀U. ⇧*[f] T ≘ U → R L U.
  46
  47 definition d_liftable1_isuni: predicate (relation2 lenv term) ≝
  48                               λR. ∀K,T. R K T → ∀b,f,L. ⇩*[b,f] L ≘ K → 𝐔❪f❫ →
  49                               ∀U. ⇧*[f] T ≘ U → R L U.
  50
  51 definition d_deliftable1: predicate (relation2 lenv term) ≝
  52                           λR. ∀L,U. R L U → ∀b,f,K. ⇩*[b,f] L ≘ K →
  53                           ∀T. ⇧*[f] T ≘ U → R K T.
  54
  55 definition d_deliftable1_isuni: predicate (relation2 lenv term) ≝
  56                                 λR. ∀L,U. R L U → ∀b,f,K. ⇩*[b,f] L ≘ K → 𝐔❪f❫ →
  57                                 ∀T. ⇧*[f] T ≘ U → R K T.
  58
  59 definition d_liftable2_sn: ∀C:Type[0]. ∀S:?→relation C.
  60                            predicate (lenv→relation C) ≝
  61                            λC,S,R. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⇩*[b,f] L ≘ K →
  62                            ∀U1. S f T1 U1 →
  63                            ∃∃U2. S f T2 U2 & R L U1 U2.
  64
  65 definition d_deliftable2_sn: ∀C:Type[0]. ∀S:?→relation C.
  66                              predicate (lenv→relation C) ≝
  67                              λC,S,R. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⇩*[b,f] L ≘ K →
  68                              ∀T1. S f T1 U1 →
  69                              ∃∃T2. S f T2 U2 & R K T1 T2.
  70
  71 definition d_liftable2_bi: ∀C:Type[0]. ∀S:?→relation C.
  72                            predicate (lenv→relation C) ≝
  73                            λC,S,R. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⇩*[b,f] L ≘ K →
  74                            ∀U1. S f T1 U1 →
  75                            ∀U2. S f T2 U2 → R L U1 U2.
  76
  77 definition d_deliftable2_bi: ∀C:Type[0]. ∀S:?→relation C.
  78                              predicate (lenv→relation C) ≝
  79                              λC,S,R. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⇩*[b,f] L ≘ K →
  80                              ∀T1. S f T1 U1 →
  81                              ∀T2. S f T2 U2 → R K T1 T2.
  82
  83 definition co_dropable_sn: predicate (?→relation lenv) ≝
  84                            λR. ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 → 𝐔❪f❫ →
  85                            ∀f2,L2. R f2 L1 L2 → ∀f1. f ~⊚ f1 ≘ f2 →
  86                            ∃∃K2. R f1 K1 K2 & ⇩*[b,f] L2 ≘ K2.
  87
  88 definition co_dropable_dx: predicate (?→relation lenv) ≝
  89                            λR. ∀f2,L1,L2. R f2 L1 L2 →
  90                            ∀b,f,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❪f❫ →
  91                            ∀f1. f ~⊚ f1 ≘ f2 →
  92                            ∃∃K1. ⇩*[b,f] L1 ≘ K1 & R f1 K1 K2.
  93
  94 definition co_dedropable_sn: predicate (?→relation lenv) ≝
  95                              λR. ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 → ∀f1,K2. R f1 K1 K2 →
  96                              ∀f2. f ~⊚ f1 ≘ f2 →
  97                              ∃∃L2. R f2 L1 L2 & ⇩*[b,f] L2 ≘ K2 & L1 ≡[f] L2.
  98
  99 (* Basic properties *********************************************************)
 100
 101 lemma drops_atom_F: ∀f. ⇩*[Ⓕ,f] ⋆ ≘ ⋆.
 102 #f @drops_atom #H destruct
 103 qed.
 104
 105 lemma drops_eq_repl_back: ∀b,L1,L2. eq_repl_back … (λf. ⇩*[b,f] L1 ≘ L2).
 106 #b #L1 #L2 #f1 #H elim H -f1 -L1 -L2
 107 [ /4 width=3 by drops_atom, isid_eq_repl_back/
 108 | #f1 #I #L1 #L2 #_ #IH #f2 #H elim (eq_inv_nx … H) -H
 109   /3 width=3 by drops_drop/
 110 | #f1 #I1 #I2 #L1 #L2 #_ #HI #IH #f2 #H elim (eq_inv_px … H) -H
 111   /3 width=3 by drops_skip, liftsb_eq_repl_back/
 112 ]
 113 qed-.
 114
 115 lemma drops_eq_repl_fwd: ∀b,L1,L2. eq_repl_fwd … (λf. ⇩*[b,f] L1 ≘ L2).
 116 #b #L1 #L2 @eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *)
 117 qed-.
 118
 119 (* Basic_2A1: includes: drop_FT *)
 120 lemma drops_TF: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → ⇩*[Ⓕ,f] L1 ≘ L2.
 121 #f #L1 #L2 #H elim H -f -L1 -L2
 122 /3 width=1 by drops_atom, drops_drop, drops_skip/
 123 qed.
 124
 125 (* Basic_2A1: includes: drop_gen *)
 126 lemma drops_gen: ∀b,f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → ⇩*[b,f] L1 ≘ L2.
 127 * /2 width=1 by drops_TF/
 128 qed-.
 129
 130 (* Basic_2A1: includes: drop_T *)
 131 lemma drops_F: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → ⇩*[Ⓕ,f] L1 ≘ L2.
 132 * /2 width=1 by drops_TF/
 133 qed-.
 134
 135 lemma d_liftable2_sn_bi: ∀C,S. (∀f,c. is_mono … (S f c)) →
 136                          ∀R. d_liftable2_sn C S R → d_liftable2_bi C S R.
 137 #C #S #HS #R #HR #K #T1 #T2 #HT12 #b #f #L #HLK #U1 #HTU1 #U2 #HTU2
 138 elim (HR … HT12 … HLK … HTU1) -HR -K -T1 #X #HTX #HUX
 139 <(HS … HTX … HTU2) -T2 -U2 -b -f //
 140 qed-.
 141
 142 lemma d_deliftable2_sn_bi: ∀C,S. (∀f. is_inj2 … (S f)) →
 143                            ∀R. d_deliftable2_sn C S R → d_deliftable2_bi C S R.
 144 #C #S #HS #R #HR #L #U1 #U2 #HU12 #b #f #K #HLK #T1 #HTU1 #T2 #HTU2
 145 elim (HR … HU12 … HLK … HTU1) -HR -L -U1 #X #HUX #HTX
 146 <(HS … HUX … HTU2) -U2 -T2 -b -f //
 147 qed-.
 148
 149 (* Basic inversion lemmas ***************************************************)
 150
 151 fact drops_inv_atom1_aux: ∀b,f,X,Y. ⇩*[b,f] X ≘ Y → X = ⋆ →
 152                           Y = ⋆ ∧ (b = Ⓣ → 𝐈❪f❫).
 153 #b #f #X #Y * -f -X -Y
 154 [ /3 width=1 by conj/
 155 | #f #I #L1 #L2 #_ #H destruct
 156 | #f #I1 #I2 #L1 #L2 #_ #_ #H destruct
 157 ]
 158 qed-.
 159
 160 (* Basic_1: includes: drop_gen_sort *)
 161 (* Basic_2A1: includes: drop_inv_atom1 *)
 162 lemma drops_inv_atom1: ∀b,f,Y. ⇩*[b,f] ⋆ ≘ Y → Y = ⋆ ∧ (b = Ⓣ → 𝐈❪f❫).
 163 /2 width=3 by drops_inv_atom1_aux/ qed-.
 164
 165 fact drops_inv_drop1_aux: ∀b,f,X,Y. ⇩*[b,f] X ≘ Y → ∀g,I,K. X = K.ⓘ[I] → f = ↑g →
 166                           ⇩*[b,g] K ≘ Y.
 167 #b #f #X #Y * -f -X -Y
 168 [ #f #Hf #g #J #K #H destruct
 169 | #f #I #L1 #L2 #HL #g #J #K #H1 #H2 <(injective_next … H2) -g destruct //
 170 | #f #I1 #I2 #L1 #L2 #_ #_ #g #J #K #_ #H2 elim (discr_push_next … H2)
 171 ]
 172 qed-.
 173
 174 (* Basic_1: includes: drop_gen_drop *)
 175 (* Basic_2A1: includes: drop_inv_drop1_lt drop_inv_drop1 *)
 176 lemma drops_inv_drop1: ∀b,f,I,K,Y. ⇩*[b,↑f] K.ⓘ[I] ≘ Y → ⇩*[b,f] K ≘ Y.
 177 /2 width=6 by drops_inv_drop1_aux/ qed-.
 178
 179 fact drops_inv_skip1_aux: ∀b,f,X,Y. ⇩*[b,f] X ≘ Y → ∀g,I1,K1. X = K1.ⓘ[I1] → f = ⫯g →
 180                           ∃∃I2,K2. ⇩*[b,g] K1 ≘ K2 & ⇧*[g] I2 ≘ I1 & Y = K2.ⓘ[I2].
 181 #b #f #X #Y * -f -X -Y
 182 [ #f #Hf #g #J1 #K1 #H destruct
 183 | #f #I #L1 #L2 #_ #g #J1 #K1 #_ #H2 elim (discr_next_push … H2)
 184 | #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_push … H2) -g destruct
 185   /2 width=5 by ex3_2_intro/
 186 ]
 187 qed-.
 188
 189 (* Basic_1: includes: drop_gen_skip_l *)
 190 (* Basic_2A1: includes: drop_inv_skip1 *)
 191 lemma drops_inv_skip1: ∀b,f,I1,K1,Y. ⇩*[b,⫯f] K1.ⓘ[I1] ≘ Y →
 192                        ∃∃I2,K2. ⇩*[b,f] K1 ≘ K2 & ⇧*[f] I2 ≘ I1 & Y = K2.ⓘ[I2].
 193 /2 width=5 by drops_inv_skip1_aux/ qed-.
 194
 195 fact drops_inv_skip2_aux: ∀b,f,X,Y. ⇩*[b,f] X ≘ Y → ∀g,I2,K2. Y = K2.ⓘ[I2] → f = ⫯g →
 196                           ∃∃I1,K1. ⇩*[b,g] K1 ≘ K2 & ⇧*[g] I2 ≘ I1 & X = K1.ⓘ[I1].
 197 #b #f #X #Y * -f -X -Y
 198 [ #f #Hf #g #J2 #K2 #H destruct
 199 | #f #I #L1 #L2 #_ #g #J2 #K2 #_ #H2 elim (discr_next_push … H2)
 200 | #f #I1 #I2 #L1 #L2 #HL #HV #g #J2 #K2 #H1 #H2 <(injective_push … H2) -g destruct
 201   /2 width=5 by ex3_2_intro/
 202 ]
 203 qed-.
 204
 205 (* Basic_1: includes: drop_gen_skip_r *)
 206 (* Basic_2A1: includes: drop_inv_skip2 *)
 207 lemma drops_inv_skip2: ∀b,f,I2,X,K2. ⇩*[b,⫯f] X ≘ K2.ⓘ[I2] →
 208                        ∃∃I1,K1. ⇩*[b,f] K1 ≘ K2 & ⇧*[f] I2 ≘ I1 & X = K1.ⓘ[I1].
 209 /2 width=5 by drops_inv_skip2_aux/ qed-.
 210
 211 (* Basic forward lemmas *****************************************************)
 212
 213 fact drops_fwd_drop2_aux: ∀b,f2,X,Y. ⇩*[b,f2] X ≘ Y → ∀I,K. Y = K.ⓘ[I] →
 214                           ∃∃f1,f. 𝐈❪f1❫ & f2 ⊚ ↑f1 ≘ f & ⇩*[b,f] X ≘ K.
 215 #b #f2 #X #Y #H elim H -f2 -X -Y
 216 [ #f2 #Hf2 #J #K #H destruct
 217 | #f2 #I #L1 #L2 #_ #IHL #J #K #H elim (IHL … H) -IHL
 218   /3 width=7 by after_next, ex3_2_intro, drops_drop/
 219 | #f2 #I1 #I2 #L1 #L2 #HL #_ #_ #J #K #H destruct
 220   lapply (after_isid_dx 𝐢 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/
 221 ]
 222 qed-.
 223
 224 lemma drops_fwd_drop2: ∀b,f2,I,X,K. ⇩*[b,f2] X ≘ K.ⓘ[I] →
 225                        ∃∃f1,f. 𝐈❪f1❫ & f2 ⊚ ↑f1 ≘ f & ⇩*[b,f] X ≘ K.
 226 /2 width=4 by drops_fwd_drop2_aux/ qed-.
 227
 228 (* Properties with test for identity ****************************************)
 229
 230 (* Basic_2A1: includes: drop_refl *)
 231 lemma drops_refl: ∀b,L,f. 𝐈❪f❫ → ⇩*[b,f] L ≘ L.
 232 #b #L elim L -L /2 width=1 by drops_atom/
 233 #L #I #IHL #f #Hf elim (isid_inv_gen … Hf) -Hf
 234 /3 width=1 by drops_skip, liftsb_refl/
 235 qed.
 236
 237 (* Forward lemmas test for identity *****************************************)
 238
 239 (* Basic_1: includes: drop_gen_refl *)
 240 (* Basic_2A1: includes: drop_inv_O2 *)
 241 lemma drops_fwd_isid: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → 𝐈❪f❫ → L1 = L2.
 242 #b #f #L1 #L2 #H elim H -f -L1 -L2 //
 243 [ #f #I #L1 #L2 #_ #_ #H elim (isid_inv_next … H) //
 244 | /5 width=5 by isid_inv_push, liftsb_fwd_isid, eq_f2, sym_eq/
 245 ]
 246 qed-.
 247
 248 lemma drops_after_fwd_drop2: ∀b,f2,I,X,K. ⇩*[b,f2] X ≘ K.ⓘ[I] →
 249                              ∀f1,f. 𝐈❪f1❫ → f2 ⊚ ↑f1 ≘ f → ⇩*[b,f] X ≘ K.
 250 #b #f2 #I #X #K #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H
 251 #g1 #g #Hg1 #Hg #HK lapply (after_mono_eq … Hg … Hf ??) -Hg -Hf
 252 /3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/
 253 qed-.
 254
 255 (* Forward lemmas with test for finite colength *****************************)
 256
 257 lemma drops_fwd_isfin: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐅❪f❫.
 258 #f #L1 #L2 #H elim H -f -L1 -L2
 259 /3 width=1 by isfin_next, isfin_push, isfin_isid/
 260 qed-.
 261
 262 (* Properties with test for uniformity **************************************)
 263
 264 lemma drops_isuni_ex: ∀f. 𝐔❪f❫ → ∀L. ∃K. ⇩*[Ⓕ,f] L ≘ K.
 265 #f #H elim H -f /4 width=2 by drops_refl, drops_TF, ex_intro/
 266 #f #_ #g #H #IH destruct * /2 width=2 by ex_intro/
 267 #L #I elim (IH L) -IH /3 width=2 by drops_drop, ex_intro/
 268 qed-.
 269
 270 (* Inversion lemmas with test for uniformity ********************************)
 271
 272 lemma drops_inv_isuni: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐔❪f❫ →
 273                        (𝐈❪f❫ ∧ L1 = L2) ∨
 274                        ∃∃g,I,K. ⇩*[Ⓣ,g] K ≘ L2 & 𝐔❪g❫ & L1 = K.ⓘ[I] & f = ↑g.
 275 #f #L1 #L2 * -f -L1 -L2
 276 [ /4 width=1 by or_introl, conj/
 277 | /4 width=7 by isuni_inv_next, ex4_3_intro, or_intror/
 278 | /7 width=6 by drops_fwd_isid, liftsb_fwd_isid, isuni_inv_push, isid_push, or_introl, conj, eq_f2, sym_eq/
 279 ]
 280 qed-.
 281
 282 (* Basic_2A1: was: drop_inv_O1_pair1 *)
 283 lemma drops_inv_bind1_isuni: ∀b,f,I,K,L2. 𝐔❪f❫ → ⇩*[b,f] K.ⓘ[I] ≘ L2 →
 284                              (𝐈❪f❫ ∧ L2 = K.ⓘ[I]) ∨
 285                              ∃∃g. 𝐔❪g❫ & ⇩*[b,g] K ≘ L2 & f = ↑g.
 286 #b #f #I #K #L2 #Hf #H elim (isuni_split … Hf) -Hf * #g #Hg #H0 destruct
 287 [ lapply (drops_inv_skip1 … H) -H * #Z #Y #HY #HZ #H destruct
 288   <(drops_fwd_isid … HY Hg) -Y >(liftsb_fwd_isid … HZ Hg) -Z
 289   /4 width=3 by isid_push, or_introl, conj/
 290 | lapply (drops_inv_drop1 … H) -H /3 width=4 by ex3_intro, or_intror/
 291 ]
 292 qed-.
 293
 294 (* Basic_2A1: was: drop_inv_O1_pair2 *)
 295 lemma drops_inv_bind2_isuni: ∀b,f,I,K,L1. 𝐔❪f❫ → ⇩*[b,f] L1 ≘ K.ⓘ[I] →
 296                              (𝐈❪f❫ ∧ L1 = K.ⓘ[I]) ∨
 297                              ∃∃g,I1,K1. 𝐔❪g❫ & ⇩*[b,g] K1 ≘ K.ⓘ[I] & L1 = K1.ⓘ[I1] & f = ↑g.
 298 #b #f #I #K *
 299 [ #Hf #H elim (drops_inv_atom1 … H) -H #H destruct
 300 | #L1 #I1 #Hf #H elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
 301   [ #Hf #H destruct /3 width=1 by or_introl, conj/
 302   | /3 width=7 by ex4_3_intro, or_intror/
 303   ]
 304 ]
 305 qed-.
 306
 307 lemma drops_inv_bind2_isuni_next: ∀b,f,I,K,L1. 𝐔❪f❫ → ⇩*[b,↑f] L1 ≘ K.ⓘ[I] →
 308                                   ∃∃I1,K1. ⇩*[b,f] K1 ≘ K.ⓘ[I] & L1 = K1.ⓘ[I1].
 309 #b #f #I #K #L1 #Hf #H elim (drops_inv_bind2_isuni … H) -H /2 width=3 by isuni_next/ -Hf *
 310 [ #H elim (isid_inv_next … H) -H //
 311 | /2 width=4 by ex2_2_intro/
 312 ]
 313 qed-.
 314
 315 fact drops_inv_TF_aux: ∀f,L1,L2. ⇩*[Ⓕ,f] L1 ≘ L2 → 𝐔❪f❫ →
 316                        ∀I,K. L2 = K.ⓘ[I] → ⇩*[Ⓣ,f] L1 ≘ K.ⓘ[I].
 317 #f #L1 #L2 #H elim H -f -L1 -L2
 318 [ #f #_ #_ #J #K #H destruct
 319 | #f #I #L1 #L2 #_ #IH #Hf #J #K #H destruct
 320   /4 width=3 by drops_drop, isuni_inv_next/
 321 | #f #I1 #I2 #L1 #L2 #HL12 #HI21 #_ #Hf #J #K #H destruct
 322   lapply (isuni_inv_push … Hf ??) -Hf [1,2: // ] #Hf
 323   <(drops_fwd_isid … HL12) -K // <(liftsb_fwd_isid … HI21) -I1
 324   /3 width=3 by drops_refl, isid_push/
 325 ]
 326 qed-.
 327
 328 (* Basic_2A1: includes: drop_inv_FT *)
 329 lemma drops_inv_TF: ∀f,I,L,K. ⇩*[Ⓕ,f] L ≘ K.ⓘ[I] → 𝐔❪f❫ → ⇩*[Ⓣ,f] L ≘ K.ⓘ[I].
 330 /2 width=3 by drops_inv_TF_aux/ qed-.
 331
 332 (* Basic_2A1: includes: drop_inv_gen *)
 333 lemma drops_inv_gen: ∀b,f,I,L,K. ⇩*[b,f] L ≘ K.ⓘ[I] → 𝐔❪f❫ → ⇩*[Ⓣ,f] L ≘ K.ⓘ[I].
 334 * /2 width=1 by drops_inv_TF/
 335 qed-.
 336
 337 (* Basic_2A1: includes: drop_inv_T *)
 338 lemma drops_inv_F: ∀b,f,I,L,K. ⇩*[Ⓕ,f] L ≘ K.ⓘ[I] → 𝐔❪f❫ → ⇩*[b,f] L ≘ K.ⓘ[I].
 339 * /2 width=1 by drops_inv_TF/
 340 qed-.
 341
 342 (* Forward lemmas with test for uniformity **********************************)
 343
 344 (* Basic_1: was: drop_S *)
 345 (* Basic_2A1: was: drop_fwd_drop2 *)
 346 lemma drops_isuni_fwd_drop2: ∀b,f,I,X,K. 𝐔❪f❫ → ⇩*[b,f] X ≘ K.ⓘ[I] → ⇩*[b,↑f] X ≘ K.
 347 /3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-.
 348
 349 (* Inversion lemmas with uniform relocations ********************************)
 350
 351 lemma drops_inv_atom2: ∀b,L,f. ⇩*[b,f] L ≘ ⋆ →
 352                        ∃∃n,f1. ⇩*[b,𝐔❨n❩] L ≘ ⋆ & 𝐔❨n❩ ⊚ f1 ≘ f.
 353 #b #L elim L -L
 354 [ /3 width=4 by drops_atom, after_isid_sn, ex2_2_intro/
 355 | #L #I #IH #f #H elim (pn_split f) * #g #H0 destruct
 356   [ elim (drops_inv_skip1 … H) -H #J #K #_ #_ #H destruct
 357   | lapply (drops_inv_drop1 … H) -H #HL
 358     elim (IH … HL) -IH -HL /3 width=8 by drops_drop, after_next, ex2_2_intro/
 359   ]
 360 ]
 361 qed-.
 362
 363 lemma drops_inv_succ: ∀L1,L2,i. ⇩[↑i] L1 ≘ L2 →
 364                       ∃∃I,K. ⇩[i] K ≘ L2 & L1 = K.ⓘ[I].
 365 #L1 #L2 #i #H elim (drops_inv_isuni … H) -H // *
 366 [ #H elim (isid_inv_next … H) -H //
 367 | /2 width=4 by ex2_2_intro/
 368 ]
 369 qed-.
 370
 371 (* Properties with uniform relocations **************************************)
 372
 373 lemma drops_F_uni: ∀L,i. ⇩*[Ⓕ,𝐔❨i❩] L ≘ ⋆ ∨ ∃∃I,K. ⇩[i] L ≘ K.ⓘ[I].
 374 #L elim L -L /2 width=1 by or_introl/
 375 #L #I #IH * /4 width=3 by drops_refl, ex1_2_intro, or_intror/
 376 #i elim (IH i) -IH /3 width=1 by drops_drop, or_introl/
 377 * /4 width=3 by drops_drop, ex1_2_intro, or_intror/
 378 qed-.
 379
 380 (* Basic_2A1: includes: drop_split *)
 381 lemma drops_split_trans: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → ∀f1,f2. f1 ⊚ f2 ≘ f → 𝐔❪f1❫ →
 382                          ∃∃L. ⇩*[b,f1] L1 ≘ L & ⇩*[b,f2] L ≘ L2.
 383 #b #f #L1 #L2 #H elim H -f -L1 -L2
 384 [ #f #H0f #f1 #f2 #Hf #Hf1 @(ex2_intro … (⋆)) @drops_atom
 385   #H lapply (H0f H) -b
 386   #H elim (after_inv_isid3 … Hf H) -f //
 387 | #f #I #L1 #L2 #HL12 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxn … Hf) -Hf [1,3: * |*: // ]
 388   [ #g1 #g2 #Hf #H1 #H2 destruct
 389     lapply (isuni_inv_push … Hf1 ??) -Hf1 [1,2: // ] #Hg1
 390     elim (IHL12 … Hf) -f
 391     /4 width=5 by drops_drop, drops_skip, liftsb_refl, isuni_isid, ex2_intro/
 392   | #g1 #Hf #H destruct elim (IHL12 … Hf) -f
 393     /3 width=5 by ex2_intro, drops_drop, isuni_inv_next/
 394   ]
 395 | #f #I1 #I2 #L1 #L2 #_ #HI21 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxp … Hf) -Hf [2,3: // ]
 396   #g1 #g2 #Hf #H1 #H2 destruct elim (liftsb_split_trans … HI21 … Hf) -HI21
 397   elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip, isuni_fwd_push/
 398 ]
 399 qed-.
 400
 401 lemma drops_split_div: ∀b,f1,L1,L. ⇩*[b,f1] L1 ≘ L → ∀f2,f. f1 ⊚ f2 ≘ f → 𝐔❪f2❫ →
 402                        ∃∃L2. ⇩*[Ⓕ,f2] L ≘ L2 & ⇩*[Ⓕ,f] L1 ≘ L2.
 403 #b #f1 #L1 #L #H elim H -f1 -L1 -L
 404 [ #f1 #Hf1 #f2 #f #Hf #Hf2 @(ex2_intro … (⋆)) @drops_atom #H destruct
 405 | #f1 #I #L1 #L #HL1 #IH #f2 #f #Hf #Hf2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
 406   #g #Hg #H destruct elim (IH … Hg) -IH -Hg /3 width=5 by drops_drop, ex2_intro/
 407 | #f1 #I1 #I #L1 #L #HL1 #HI1 #IH #f2 #f #Hf #Hf2
 408   elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ]
 409   #g2 #g #Hg #H2 #H0 destruct
 410   [ lapply (isuni_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH
 411     lapply (after_isid_inv_dx … Hg … Hg2) -Hg #Hg
 412     /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, liftsb_eq_repl_back, isid_push, ex2_intro/
 413   | lapply (isuni_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HI1
 414     elim (IH … Hg) -f1 /3 width=3 by drops_drop, ex2_intro/
 415   ]
 416 ]
 417 qed-.
 418
 419 (* Properties with application **********************************************)
 420
 421 lemma drops_tls_at: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
 422                     ∀b,L1,L2. ⇩*[b,⫰*[i2]f] L1 ≘ L2 →
 423                     ⇩*[b,⫯⫰*[↑i2]f] L1 ≘ L2.
 424 /3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-.
 425
 426 lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⇩*[b,f] L ≘ K0.ⓘ[I] → ∀i. @❪O,f❫ ≘ i →
 427                                ∃∃J,K. ⇩[i]L ≘ K.ⓘ[J] & ⇩*[b,⫰*[↑i]f] K ≘ K0 & ⇧*[⫰*[↑i]f] I ≘ J.
 428 #b #f #I #L #K0 #H #i #Hf
 429 elim (drops_split_trans … H) -H [ |5: @(after_uni_dx … Hf) |2,3: skip ] /2 width=1 by after_isid_dx/ #Y #HLY #H
 430 lapply (drops_tls_at … Hf … H) -H #H
 431 elim (drops_inv_skip2 … H) -H #J #K #HK0 #HIJ #H destruct
 432 /3 width=5 by drops_inv_gen, ex3_2_intro/
 433 qed-.
 434
 435 (* Properties with context-sensitive equivalence for terms ******************)
 436
 437 lemma ceq_lift_sn: d_liftable2_sn … liftsb ceq_ext.
 438 #K #I1 #I2 #H <(ceq_ext_inv_eq … H) -I2
 439 /2 width=3 by ex2_intro/ qed-.
 440
 441 lemma ceq_inv_lift_sn: d_deliftable2_sn … liftsb ceq_ext.
 442 #L #J1 #J2 #H <(ceq_ext_inv_eq … H) -J2
 443 /2 width=3 by ex2_intro/ qed-.
 444
 445 (* Note: d_deliftable2_sn cfull does not hold *)
 446 lemma cfull_lift_sn: d_liftable2_sn … liftsb cfull.
 447 #K #I1 #I2 #_ #b #f #L #_ #J1 #_ -K -I1 -b
 448 elim (liftsb_total I2 f) /2 width=3 by ex2_intro/
 449 qed-.
 450
 451 (* Basic_2A1: removed theorems 12:
 452               drops_inv_nil drops_inv_cons d1_liftable_liftables
 453               drop_refl_atom_O2 drop_inv_pair1
 454               drop_inv_Y1 drop_Y1 drop_O_Y drop_fwd_Y2
 455               drop_fwd_length_minus2 drop_fwd_length_minus4
 456 *)
 457 (* Basic_1: removed theorems 53:
 458             drop1_gen_pnil drop1_gen_pcons drop1_getl_trans
 459             drop_ctail drop_skip_flat
 460             cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
 461             drop_clear drop_clear_O drop_clear_S
 462             clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r
 463             clear_gen_all clear_clear clear_mono clear_trans clear_ctail clear_cle
 464             getl_ctail_clen getl_gen_tail clear_getl_trans getl_clear_trans
 465             getl_clear_bind getl_clear_conf getl_dec getl_drop getl_drop_conf_lt
 466             getl_drop_conf_ge getl_conf_ge_drop getl_drop_conf_rev
 467             drop_getl_trans_lt drop_getl_trans_le drop_getl_trans_ge
 468             getl_drop_trans getl_flt getl_gen_all getl_gen_sort getl_gen_O
 469             getl_gen_S getl_gen_2 getl_gen_flat getl_gen_bind getl_conf_le
 470             getl_trans getl_refl getl_head getl_flat getl_ctail getl_mono
 471 *)