matita/matita/contribs/lambdadelta/static_2/static/lsubf.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_3_3.ma".
  16 include "ground/xoa/ex_4_3.ma".
  17 include "ground/xoa/ex_5_5.ma".
  18 include "ground/xoa/ex_5_6.ma".
  19 include "ground/xoa/ex_6_5.ma".
  20 include "ground/xoa/ex_7_6.ma".
  21 include "static_2/notation/relations/lrsubeqf_4.ma".
  22 include "ground/relocation/nstream_sor.ma".
  23 include "static_2/static/frees.ma".
  24
  25 (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
  26
  27 inductive lsubf: relation4 lenv rtmap lenv rtmap ≝
  28 | lsubf_atom: ∀f1,f2. f1 ≡ f2 → lsubf (⋆) f1 (⋆) f2
  29 | lsubf_push: ∀f1,f2,I1,I2,L1,L2. lsubf L1 (f1) L2 (f2) →
  30               lsubf (L1.ⓘ[I1]) (⫯f1) (L2.ⓘ[I2]) (⫯f2)
  31 | lsubf_bind: ∀f1,f2,I,L1,L2. lsubf L1 f1 L2 f2 →
  32               lsubf (L1.ⓘ[I]) (↑f1) (L2.ⓘ[I]) (↑f2)
  33 | lsubf_beta: ∀f,f0,f1,f2,L1,L2,W,V. L1 ⊢ 𝐅+❪V❫ ≘ f → f0 ⋓ f ≘ f1 →
  34               lsubf L1 f0 L2 f2 → lsubf (L1.ⓓⓝW.V) (↑f1) (L2.ⓛW) (↑f2)
  35 | lsubf_unit: ∀f,f0,f1,f2,I1,I2,L1,L2,V. L1 ⊢ 𝐅+❪V❫ ≘ f → f0 ⋓ f ≘ f1 →
  36               lsubf L1 f0 L2 f2 → lsubf (L1.ⓑ[I1]V) (↑f1) (L2.ⓤ[I2]) (↑f2)
  37 .
  38
  39 interpretation
  40   "local environment refinement (context-sensitive free variables)"
  41   'LRSubEqF L1 f1 L2 f2 = (lsubf L1 f1 L2 f2).
  42
  43 (* Basic inversion lemmas ***************************************************)
  44
  45 fact lsubf_inv_atom1_aux:
  46      ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → L1 = ⋆ →
  47      ∧∧ f1 ≡ f2 & L2 = ⋆.
  48 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  49 [ /2 width=1 by conj/
  50 | #f1 #f2 #I1 #I2 #L1 #L2 #_ #H destruct
  51 | #f1 #f2 #I #L1 #L2 #_ #H destruct
  52 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
  53 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #H destruct
  54 ]
  55 qed-.
  56
  57 lemma lsubf_inv_atom1: ∀f1,f2,L2. ❪⋆,f1❫ ⫃𝐅+ ❪L2,f2❫ → ∧∧ f1 ≡ f2 & L2 = ⋆.
  58 /2 width=3 by lsubf_inv_atom1_aux/ qed-.
  59
  60 fact lsubf_inv_push1_aux:
  61      ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ →
  62      ∀g1,I1,K1. f1 = ⫯g1 → L1 = K1.ⓘ[I1] →
  63      ∃∃g2,I2,K2. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f2 = ⫯g2 & L2 = K2.ⓘ[I2].
  64 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  65 [ #f1 #f2 #_ #g1 #J1 #K1 #_ #H destruct
  66 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J1 #K1 #H1 #H2 destruct
  67   <(injective_push … H1) -g1 /2 width=6 by ex3_3_intro/
  68 | #f1 #f2 #I #L1 #L2 #_ #g1 #J1 #K1 #H elim (discr_next_push … H)
  69 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J1 #K1 #H elim (discr_next_push … H)
  70 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J1 #K1 #H elim (discr_next_push … H)
  71 ]
  72 qed-.
  73
  74 lemma lsubf_inv_push1:
  75       ∀g1,f2,I1,K1,L2. ❪K1.ⓘ[I1],⫯g1❫ ⫃𝐅+ ❪L2,f2❫ →
  76       ∃∃g2,I2,K2. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f2 = ⫯g2 & L2 = K2.ⓘ[I2].
  77 /2 width=6 by lsubf_inv_push1_aux/ qed-.
  78
  79 fact lsubf_inv_pair1_aux:
  80      ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ →
  81      ∀g1,I,K1,X. f1 = ↑g1 → L1 = K1.ⓑ[I]X →
  82      ∨∨ ∃∃g2,K2. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f2 = ↑g2 & L2 = K2.ⓑ[I]X
  83       | ∃∃g,g0,g2,K2,W,V. ❪K1,g0❫ ⫃𝐅+ ❪K2,g2❫ &
  84           K1 ⊢ 𝐅+❪V❫ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 &
  85           I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
  86       | ∃∃g,g0,g2,J,K2. ❪K1,g0❫ ⫃𝐅+ ❪K2,g2❫ &
  87           K1 ⊢ 𝐅+❪X❫ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 & L2 = K2.ⓤ[J].
  88 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  89 [ #f1 #f2 #_ #g1 #J #K1 #X #_ #H destruct
  90 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #X #H elim (discr_push_next … H)
  91 | #f1 #f2 #I #L1 #L2 #H12 #g1 #J #K1 #X #H1 #H2 destruct
  92   <(injective_next … H1) -g1 /3 width=5 by or3_intro0, ex3_2_intro/
  93 | #f #f0 #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H12 #g1 #J #K1 #X #H1 #H2 destruct
  94   <(injective_next … H1) -g1 /3 width=12 by or3_intro1, ex7_6_intro/
  95 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #Hf #Hf1 #H12 #g1 #J #K1 #X #H1 #H2 destruct
  96   <(injective_next … H1) -g1 /3 width=10 by or3_intro2, ex5_5_intro/
  97 ]
  98 qed-.
  99
 100 lemma lsubf_inv_pair1:
 101       ∀g1,f2,I,K1,L2,X. ❪K1.ⓑ[I]X,↑g1❫ ⫃𝐅+ ❪L2,f2❫ →
 102       ∨∨ ∃∃g2,K2. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f2 = ↑g2 & L2 = K2.ⓑ[I]X
 103        | ∃∃g,g0,g2,K2,W,V. ❪K1,g0❫ ⫃𝐅+ ❪K2,g2❫ &
 104            K1 ⊢ 𝐅+❪V❫ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 &
 105            I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
 106        | ∃∃g,g0,g2,J,K2. ❪K1,g0❫ ⫃𝐅+ ❪K2,g2❫ &
 107            K1 ⊢ 𝐅+❪X❫ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 & L2 = K2.ⓤ[J].
 108 /2 width=5 by lsubf_inv_pair1_aux/ qed-.
 109
 110 fact lsubf_inv_unit1_aux:
 111      ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ →
 112      ∀g1,I,K1. f1 = ↑g1 → L1 = K1.ⓤ[I] →
 113      ∃∃g2,K2. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f2 = ↑g2 & L2 = K2.ⓤ[I].
 114 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 115 [ #f1 #f2 #_ #g1 #J #K1 #_ #H destruct
 116 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #H elim (discr_push_next … H)
 117 | #f1 #f2 #I #L1 #L2 #H12 #g1 #J #K1 #H1 #H2 destruct
 118   <(injective_next … H1) -g1 /2 width=5 by ex3_2_intro/
 119 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #_ #H destruct
 120 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J #K1 #_ #H destruct
 121 ]
 122 qed-.
 123
 124 lemma lsubf_inv_unit1:
 125       ∀g1,f2,I,K1,L2. ❪K1.ⓤ[I],↑g1❫ ⫃𝐅+ ❪L2,f2❫ →
 126       ∃∃g2,K2. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f2 = ↑g2 & L2 = K2.ⓤ[I].
 127 /2 width=5 by lsubf_inv_unit1_aux/ qed-.
 128
 129 fact lsubf_inv_atom2_aux:
 130      ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → L2 = ⋆ →
 131      ∧∧ f1 ≡ f2 & L1 = ⋆.
 132 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 133 [ /2 width=1 by conj/
 134 | #f1 #f2 #I1 #I2 #L1 #L2 #_ #H destruct
 135 | #f1 #f2 #I #L1 #L2 #_ #H destruct
 136 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
 137 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #H destruct
 138 ]
 139 qed-.
 140
 141 lemma lsubf_inv_atom2: ∀f1,f2,L1. ❪L1,f1❫ ⫃𝐅+ ❪⋆,f2❫ → ∧∧f1 ≡ f2 & L1 = ⋆.
 142 /2 width=3 by lsubf_inv_atom2_aux/ qed-.
 143
 144 fact lsubf_inv_push2_aux:
 145      ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ →
 146      ∀g2,I2,K2. f2 = ⫯g2 → L2 = K2.ⓘ[I2] →
 147      ∃∃g1,I1,K1. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f1 = ⫯g1 & L1 = K1.ⓘ[I1].
 148 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 149 [ #f1 #f2 #_ #g2 #J2 #K2 #_ #H destruct
 150 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J2 #K2 #H1 #H2 destruct
 151   <(injective_push … H1) -g2 /2 width=6 by ex3_3_intro/
 152 | #f1 #f2 #I #L1 #L2 #_ #g2 #J2 #K2 #H elim (discr_next_push … H)
 153 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J2 #K2 #H elim (discr_next_push … H)
 154 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J2 #K2 #H elim (discr_next_push … H)
 155 ]
 156 qed-.
 157
 158 lemma lsubf_inv_push2:
 159       ∀f1,g2,I2,L1,K2. ❪L1,f1❫ ⫃𝐅+ ❪K2.ⓘ[I2],⫯g2❫ →
 160       ∃∃g1,I1,K1. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f1 = ⫯g1 & L1 = K1.ⓘ[I1].
 161 /2 width=6 by lsubf_inv_push2_aux/ qed-.
 162
 163 fact lsubf_inv_pair2_aux:
 164      ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ →
 165      ∀g2,I,K2,W. f2 = ↑g2 → L2 = K2.ⓑ[I]W →
 166      ∨∨ ∃∃g1,K1. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f1 = ↑g1 & L1 = K1.ⓑ[I]W
 167       | ∃∃g,g0,g1,K1,V. ❪K1,g0❫ ⫃𝐅+ ❪K2,g2❫ &
 168           K1 ⊢ 𝐅+❪V❫ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 &
 169           I = Abst & L1 = K1.ⓓⓝW.V.
 170 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 171 [ #f1 #f2 #_ #g2 #J #K2 #X #_ #H destruct
 172 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #X #H elim (discr_push_next … H)
 173 | #f1 #f2 #I #L1 #L2 #H12 #g2 #J #K2 #X #H1 #H2 destruct
 174   <(injective_next … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/
 175 | #f #f0 #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H12 #g2 #J #K2 #X #H1 #H2 destruct
 176   <(injective_next … H1) -g2 /3 width=10 by ex6_5_intro, or_intror/
 177 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J #K2 #X #_ #H destruct
 178 ]
 179 qed-.
 180
 181 lemma lsubf_inv_pair2:
 182       ∀f1,g2,I,L1,K2,W. ❪L1,f1❫ ⫃𝐅+ ❪K2.ⓑ[I]W,↑g2❫ →
 183       ∨∨ ∃∃g1,K1. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f1 = ↑g1 & L1 = K1.ⓑ[I]W
 184        | ∃∃g,g0,g1,K1,V. ❪K1,g0❫ ⫃𝐅+ ❪K2,g2❫ &
 185            K1 ⊢ 𝐅+❪V❫ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 &
 186            I = Abst & L1 = K1.ⓓⓝW.V.
 187 /2 width=5 by lsubf_inv_pair2_aux/ qed-.
 188
 189 fact lsubf_inv_unit2_aux:
 190      ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ →
 191      ∀g2,I,K2. f2 = ↑g2 → L2 = K2.ⓤ[I] →
 192      ∨∨ ∃∃g1,K1. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f1 = ↑g1 & L1 = K1.ⓤ[I]
 193       | ∃∃g,g0,g1,J,K1,V. ❪K1,g0❫ ⫃𝐅+ ❪K2,g2❫ &
 194           K1 ⊢ 𝐅+❪V❫ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 & L1 = K1.ⓑ[J]V.
 195 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 196 [ #f1 #f2 #_ #g2 #J #K2 #_ #H destruct
 197 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #H elim (discr_push_next … H)
 198 | #f1 #f2 #I #L1 #L2 #H12 #g2 #J #K2 #H1 #H2 destruct
 199   <(injective_next … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/
 200 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #_ #H destruct
 201 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #Hf #Hf1 #H12 #g2 #J #K2 #H1 #H2 destruct
 202   <(injective_next … H1) -g2 /3 width=11 by ex5_6_intro, or_intror/
 203 ]
 204 qed-.
 205
 206 lemma lsubf_inv_unit2:
 207       ∀f1,g2,I,L1,K2. ❪L1,f1❫ ⫃𝐅+ ❪K2.ⓤ[I],↑g2❫ →
 208       ∨∨ ∃∃g1,K1. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f1 = ↑g1 & L1 = K1.ⓤ[I]
 209        | ∃∃g,g0,g1,J,K1,V. ❪K1,g0❫ ⫃𝐅+ ❪K2,g2❫ &
 210            K1 ⊢ 𝐅+❪V❫ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 & L1 = K1.ⓑ[J]V.
 211 /2 width=5 by lsubf_inv_unit2_aux/ qed-.
 212
 213 (* Advanced inversion lemmas ************************************************)
 214
 215 lemma lsubf_inv_atom: ∀f1,f2. ❪⋆,f1❫ ⫃𝐅+ ❪⋆,f2❫ → f1 ≡ f2.
 216 #f1 #f2 #H elim (lsubf_inv_atom1 … H) -H //
 217 qed-.
 218
 219 lemma lsubf_inv_push_sn:
 220       ∀g1,f2,I1,I2,K1,K2. ❪K1.ⓘ[I1],⫯g1❫ ⫃𝐅+ ❪K2.ⓘ[I2],f2❫ →
 221       ∃∃g2. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f2 = ⫯g2.
 222 #g1 #f2 #I #K1 #K2 #X #H elim (lsubf_inv_push1 … H) -H
 223 #g2 #I #Y #H0 #H2 #H destruct /2 width=3 by ex2_intro/
 224 qed-.
 225
 226 lemma lsubf_inv_bind_sn:
 227       ∀g1,f2,I,K1,K2. ❪K1.ⓘ[I],↑g1❫ ⫃𝐅+ ❪K2.ⓘ[I],f2❫ →
 228       ∃∃g2. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f2 = ↑g2.
 229 #g1 #f2 * #I [2: #X ] #K1 #K2 #H
 230 [ elim (lsubf_inv_pair1 … H) -H *
 231   [ #z2 #Y2 #H2 #H #H0 destruct /2 width=3 by ex2_intro/
 232   | #z #z0 #z2 #Y2 #W #V #_ #_ #_ #_ #H0 #_ #H destruct
 233   | #z #z0 #z2 #Z2 #Y2 #_ #_ #_ #_ #H destruct
 234   ]
 235 | elim (lsubf_inv_unit1 … H) -H
 236   #z2 #Y2 #H2 #H #H0 destruct /2 width=3 by ex2_intro/
 237 ]
 238 qed-.
 239
 240 lemma lsubf_inv_beta_sn:
 241       ∀g1,f2,K1,K2,V,W. ❪K1.ⓓⓝW.V,↑g1❫ ⫃𝐅+ ❪K2.ⓛW,f2❫ →
 242       ∃∃g,g0,g2. ❪K1,g0❫ ⫃𝐅+ ❪K2,g2❫ & K1 ⊢ 𝐅+❪V❫ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2.
 243 #g1 #f2 #K1 #K2 #V #W #H elim (lsubf_inv_pair1 … H) -H *
 244 [ #z2 #Y2 #_ #_ #H destruct
 245 | #z #z0 #z2 #Y2 #X0 #X #H02 #Hz #Hg1 #H #_ #H0 #H1 destruct
 246   /2 width=7 by ex4_3_intro/
 247 | #z #z0 #z2 #Z2 #Y2 #_ #_ #_ #_ #H destruct
 248 ]
 249 qed-.
 250
 251 lemma lsubf_inv_unit_sn:
 252       ∀g1,f2,I,J,K1,K2,V. ❪K1.ⓑ[I]V,↑g1❫ ⫃𝐅+ ❪K2.ⓤ[J],f2❫ →
 253       ∃∃g,g0,g2. ❪K1,g0❫ ⫃𝐅+ ❪K2,g2❫ & K1 ⊢ 𝐅+❪V❫ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2.
 254 #g1 #f2 #I #J #K1 #K2 #V #H elim (lsubf_inv_pair1 … H) -H *
 255 [ #z2 #Y2 #_ #_ #H destruct
 256 | #z #z0 #z2 #Y2 #X0 #X #_ #_ #_ #_ #_ #_ #H destruct
 257 | #z #z0 #z2 #Z2 #Y2 #H02 #Hz #Hg1 #H0 #H1 destruct
 258   /2 width=7 by ex4_3_intro/
 259 ]
 260 qed-.
 261
 262 lemma lsubf_inv_refl: ∀L,f1,f2. ❪L,f1❫ ⫃𝐅+ ❪L,f2❫ → f1 ≡ f2.
 263 #L elim L -L /2 width=1 by lsubf_inv_atom/
 264 #L #I #IH #f1 #f2 #H12
 265 elim (pn_split f1) * #g1 #H destruct
 266 [ elim (lsubf_inv_push_sn … H12) | elim (lsubf_inv_bind_sn … H12) ] -H12
 267 #g2 #H12 #H destruct /3 width=5 by eq_next, eq_push/
 268 qed-.
 269
 270 (* Basic forward lemmas *****************************************************)
 271
 272 lemma lsubf_fwd_bind_tl:
 273       ∀f1,f2,I,L1,L2. ❪L1.ⓘ[I],f1❫ ⫃𝐅+ ❪L2.ⓘ[I],f2❫ → ❪L1,⫰f1❫ ⫃𝐅+ ❪L2,⫰f2❫.
 274 #f1 #f2 #I #L1 #L2 #H
 275 elim (pn_split f1) * #g1 #H0 destruct
 276 [ elim (lsubf_inv_push_sn … H) | elim (lsubf_inv_bind_sn … H) ] -H
 277 #g2 #H12 #H destruct //
 278 qed-.
 279
 280 lemma lsubf_fwd_isid_dx: ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → 𝐈❪f2❫ → 𝐈❪f1❫.
 281 #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
 282 [ /2 width=3 by isid_eq_repl_fwd/
 283 | /4 width=3 by isid_inv_push, isid_push/
 284 | #f1 #f2 #I #L1 #L2 #_ #_ #H elim (isid_inv_next … H) -H //
 285 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
 286 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
 287 ]
 288 qed-.
 289
 290 lemma lsubf_fwd_isid_sn: ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → 𝐈❪f1❫ → 𝐈❪f2❫.
 291 #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
 292 [ /2 width=3 by isid_eq_repl_back/
 293 | /4 width=3 by isid_inv_push, isid_push/
 294 | #f1 #f2 #I #L1 #L2 #_ #_ #H elim (isid_inv_next … H) -H //
 295 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
 296 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
 297 ]
 298 qed-.
 299
 300 lemma lsubf_fwd_sle: ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → f2 ⊆ f1.
 301 #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
 302 /3 width=5 by sor_inv_sle_sn_trans, sle_next, sle_push, sle_refl_eq, eq_sym/
 303 qed-.
 304
 305 (* Basic properties *********************************************************)
 306
 307 lemma lsubf_eq_repl_back1: ∀f2,L1,L2. eq_repl_back … (λf1. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
 308 #f2 #L1 #L2 #f #H elim H -f -f2 -L1 -L2
 309 [ #f1 #f2 #Hf12 #g1 #Hfg1
 310   /3 width=3 by lsubf_atom, eq_canc_sn/
 311 | #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H
 312   elim (eq_inv_px … H) -H [|*: // ] #g1 #Hfg1 #H destruct
 313   /3 width=1 by lsubf_push/
 314 | #f1 #f2 #I #K1 #K2 #_ #IH #g #H
 315   elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct
 316   /3 width=1 by lsubf_bind/
 317 | #f #f0 #f1 #f2 #K1 #L2 #W #V #Hf #Hf1 #_ #IH #g #H
 318   elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct
 319   /3 width=5 by lsubf_beta, sor_eq_repl_back3/
 320 | #f #f0 #f1 #f2 #I1 #I2 #K1 #K2 #V #Hf #Hf1 #_ #IH #g #H
 321   elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct
 322   /3 width=5 by lsubf_unit, sor_eq_repl_back3/
 323 ]
 324 qed-.
 325
 326 lemma lsubf_eq_repl_fwd1: ∀f2,L1,L2. eq_repl_fwd … (λf1. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
 327 #f2 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back1/
 328 qed-.
 329
 330 lemma lsubf_eq_repl_back2: ∀f1,L1,L2. eq_repl_back … (λf2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
 331 #f1 #L1 #L2 #f #H elim H -f1 -f -L1 -L2
 332 [ #f1 #f2 #Hf12 #g2 #Hfg2
 333   /3 width=3 by lsubf_atom, eq_trans/
 334 | #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H
 335   elim (eq_inv_px … H) -H [|*: // ] #g2 #Hfg2 #H destruct
 336   /3 width=1 by lsubf_push/
 337 | #f1 #f2 #I #K1 #K2 #_ #IH #g #H
 338   elim (eq_inv_nx … H) -H [|*: // ] #g2 #Hfg2 #H destruct
 339   /3 width=1 by lsubf_bind/
 340 | #f #f0 #f1 #f2 #K1 #L2 #W #V #Hf #Hf1 #_ #IH #g #H
 341   elim (eq_inv_nx … H) -H [|*: // ] #g2 #Hfg2 #H destruct
 342   /3 width=5 by lsubf_beta/
 343 | #f #f0 #f1 #f2 #I1 #I2 #K1 #K2 #V #Hf #Hf1 #_ #IH #g #H
 344   elim (eq_inv_nx … H) -H [|*: // ] #g2 #Hfg2 #H destruct
 345   /3 width=5 by lsubf_unit/
 346 ]
 347 qed-.
 348
 349 lemma lsubf_eq_repl_fwd2: ∀f1,L1,L2. eq_repl_fwd … (λf2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
 350 #f1 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back2/
 351 qed-.
 352
 353 lemma lsubf_refl: bi_reflexive … lsubf.
 354 #L elim L -L /2 width=1 by lsubf_atom, eq_refl/
 355 #L #I #IH #f elim (pn_split f) * #g #H destruct
 356 /2 width=1 by lsubf_push, lsubf_bind/
 357 qed.
 358
 359 lemma lsubf_refl_eq: ∀f1,f2,L. f1 ≡ f2 → ❪L,f1❫ ⫃𝐅+ ❪L,f2❫.
 360 /2 width=3 by lsubf_eq_repl_back2/ qed.
 361
 362 lemma lsubf_bind_tl_dx:
 363       ∀g1,f2,I,L1,L2. ❪L1,g1❫ ⫃𝐅+ ❪L2,⫰f2❫ →
 364       ∃∃f1. ❪L1.ⓘ[I],f1❫ ⫃𝐅+ ❪L2.ⓘ[I],f2❫ & g1 = ⫰f1.
 365 #g1 #f2 #I #L1 #L2 #H
 366 elim (pn_split f2) * #g2 #H2 destruct
 367 @ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *)
 368 qed-.
 369
 370 lemma lsubf_beta_tl_dx:
 371       ∀f,f0,g1,L1,V. L1 ⊢ 𝐅+❪V❫ ≘ f → f0 ⋓ f ≘ g1 →
 372       ∀f2,L2,W. ❪L1,f0❫ ⫃𝐅+ ❪L2,⫰f2❫ →
 373       ∃∃f1. ❪L1.ⓓⓝW.V,f1❫ ⫃𝐅+ ❪L2.ⓛW,f2❫ & ⫰f1 ⊆ g1.
 374 #f #f0 #g1 #L1 #V #Hf #Hg1 #f2
 375 elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct
 376 [ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/
 377 | @(ex2_intro … (↑g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *)
 378 ]
 379 qed-.
 380
 381 (* Note: this might be moved *)
 382 lemma lsubf_inv_sor_dx:
 383       ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ →
 384       ∀f2l,f2r. f2l⋓f2r ≘ f2 →
 385       ∃∃f1l,f1r. ❪L1,f1l❫ ⫃𝐅+ ❪L2,f2l❫ & ❪L1,f1r❫ ⫃𝐅+ ❪L2,f2r❫ & f1l⋓f1r ≘ f1.
 386 #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
 387 [ /3 width=7 by sor_eq_repl_fwd3, ex3_2_intro/
 388 | #g1 #g2 #I1 #I2 #L1 #L2 #_ #IH #f2l #f2r #H
 389   elim (sor_inv_xxp … H) -H [|*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
 390   elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, sor_pp, ex3_2_intro/
 391 | #g1 #g2 #I #L1 #L2 #_ #IH #f2l #f2r #H
 392   elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
 393   elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, lsubf_bind, sor_np, sor_pn, sor_nn, ex3_2_intro/
 394 | #g #g0 #g1 #g2 #L1 #L2 #W #V #Hg #Hg1 #_ #IH #f2l #f2r #H
 395   elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
 396   elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0
 397   [ lapply (sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
 398     /3 width=11 by lsubf_push, lsubf_beta, sor_np, ex3_2_intro/
 399   | lapply (sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
 400     /3 width=11 by lsubf_push, lsubf_beta, sor_pn, ex3_2_intro/
 401   | lapply (sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
 402     /3 width=11 by lsubf_beta, sor_nn, ex3_2_intro/
 403   ]
 404 | #g #g0 #g1 #g2 #I1 #I2 #L1 #L2 #V #Hg #Hg1 #_ #IH #f2l #f2r #H
 405   elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
 406   elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0
 407   [ lapply (sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
 408     /3 width=11 by lsubf_push, lsubf_unit, sor_np, ex3_2_intro/
 409   | lapply (sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
 410     /3 width=11 by lsubf_push, lsubf_unit, sor_pn, ex3_2_intro/
 411   | lapply (sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
 412     /3 width=11 by lsubf_unit, sor_nn, ex3_2_intro/
 413   ]
 414 ]
 415 qed-.