matita/matita/contribs/lambdadelta/basic_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 "basic_2/notation/relations/lrsubeqf_4.ma".
  16 include "basic_2/static/frees.ma".
  17
  18 (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
  19
  20 inductive lsubf: relation4 lenv rtmap lenv rtmap ≝
  21 | lsubf_atom: ∀f1,f2. f1 ≗ f2 → lsubf (⋆) f1 (⋆) f2
  22 | lsubf_push: ∀f1,f2,I1,I2,L1,L2. lsubf L1 (f1) L2 (f2) →
  23               lsubf (L1.ⓘ{I1}) (↑f1) (L2.ⓘ{I2}) (↑f2)
  24 | lsubf_bind: ∀f1,f2,I,L1,L2. lsubf L1 f1 L2 f2 →
  25               lsubf (L1.ⓘ{I}) (⫯f1) (L2.ⓘ{I}) (⫯f2)
  26 | lsubf_beta: ∀f,f0,f1,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f0 ⋓ f ≡ f1 →
  27               lsubf L1 f0 L2 f2 → lsubf (L1.ⓓⓝW.V) (⫯f1) (L2.ⓛW) (⫯f2)
  28 | lsubf_unit: ∀f,f0,f1,f2,I1,I2,L1,L2,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f0 ⋓ f ≡ f1 →
  29               lsubf L1 f0 L2 f2 → lsubf (L1.ⓑ{I1}V) (⫯f1) (L2.ⓤ{I2}) (⫯f2)
  30 .
  31
  32 interpretation
  33   "local environment refinement (context-sensitive free variables)"
  34   'LRSubEqF L1 f1 L2 f2 = (lsubf L1 f1 L2 f2).
  35
  36 (* Basic inversion lemmas ***************************************************)
  37
  38 fact lsubf_inv_atom1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L1 = ⋆ →
  39                           f1 ≗ f2 ∧ L2 = ⋆.
  40 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  41 [ /2 width=1 by conj/
  42 | #f1 #f2 #I1 #I2 #L1 #L2 #_ #H destruct
  43 | #f1 #f2 #I #L1 #L2 #_ #H destruct
  44 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
  45 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #H destruct
  46 ]
  47 qed-.
  48
  49 lemma lsubf_inv_atom1: ∀f1,f2,L2. ⦃⋆, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → f1 ≗ f2 ∧ L2 = ⋆.
  50 /2 width=3 by lsubf_inv_atom1_aux/ qed-.
  51
  52 fact lsubf_inv_push1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  53                           ∀g1,I1,K1. f1 = ↑g1 → L1 = K1.ⓘ{I1} →
  54                           ∃∃g2,I2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2 & L2 = K2.ⓘ{I2}.
  55 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  56 [ #f1 #f2 #_ #g1 #J1 #K1 #_ #H destruct
  57 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J1 #K1 #H1 #H2 destruct
  58   <(injective_push … H1) -g1 /2 width=6 by ex3_3_intro/
  59 | #f1 #f2 #I #L1 #L2 #_ #g1 #J1 #K1 #H elim (discr_next_push … H)
  60 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J1 #K1 #H elim (discr_next_push … H)
  61 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J1 #K1 #H elim (discr_next_push … H)
  62 ]
  63 qed-.
  64
  65 lemma lsubf_inv_push1: ∀g1,f2,I1,K1,L2. ⦃K1.ⓘ{I1}, ↑g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  66                        ∃∃g2,I2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2 & L2 = K2.ⓘ{I2}.
  67 /2 width=6 by lsubf_inv_push1_aux/ qed-.
  68
  69 fact lsubf_inv_pair1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  70                           ∀g1,I,K1,X. f1 = ⫯g1 → L1 = K1.ⓑ{I}X →
  71                           ∨∨ ∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X
  72                            | ∃∃g,g0,g2,K2,W,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
  73                                                K1 ⊢ 𝐅*⦃V⦄ ≡ g & g0 ⋓ g ≡ g1 & f2 = ⫯g2 &
  74                                                I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
  75                            | ∃∃g,g0,g2,J,K2. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
  76                                              K1 ⊢ 𝐅*⦃X⦄ ≡ g & g0 ⋓ g ≡ g1 & f2 = ⫯g2 &
  77                                              L2 = K2.ⓤ{J}.
  78 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
  79 [ #f1 #f2 #_ #g1 #J #K1 #X #_ #H destruct
  80 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #X #H elim (discr_push_next … H)
  81 | #f1 #f2 #I #L1 #L2 #H12 #g1 #J #K1 #X #H1 #H2 destruct
  82   <(injective_next … H1) -g1 /3 width=5 by or3_intro0, ex3_2_intro/
  83 | #f #f0 #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H12 #g1 #J #K1 #X #H1 #H2 destruct
  84   <(injective_next … H1) -g1 /3 width=12 by or3_intro1, ex7_6_intro/
  85 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #Hf #Hf1 #H12 #g1 #J #K1 #X #H1 #H2 destruct
  86   <(injective_next … H1) -g1 /3 width=10 by or3_intro2, ex5_5_intro/
  87 ]
  88 qed-.
  89
  90 lemma lsubf_inv_pair1: ∀g1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, ⫯g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
  91                        ∨∨ ∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X
  92                         | ∃∃g,g0,g2,K2,W,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
  93                                             K1 ⊢ 𝐅*⦃V⦄ ≡ g & g0 ⋓ g ≡ g1 & f2 = ⫯g2 &
  94                                             I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
  95                         | ∃∃g,g0,g2,J,K2. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
  96                                           K1 ⊢ 𝐅*⦃X⦄ ≡ g & g0 ⋓ g ≡ g1 & f2 = ⫯g2 &
  97                                           L2 = K2.ⓤ{J}.
  98 /2 width=5 by lsubf_inv_pair1_aux/ qed-.
  99
 100 fact lsubf_inv_unit1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
 101                           ∀g1,I,K1. f1 = ⫯g1 → L1 = K1.ⓤ{I} →
 102                           ∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓤ{I}.
 103 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 104 [ #f1 #f2 #_ #g1 #J #K1 #_ #H destruct
 105 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #H elim (discr_push_next … H)
 106 | #f1 #f2 #I #L1 #L2 #H12 #g1 #J #K1 #H1 #H2 destruct
 107   <(injective_next … H1) -g1 /2 width=5 by ex3_2_intro/
 108 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #_ #H destruct
 109 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J #K1 #_ #H destruct
 110 ]
 111 qed-.
 112
 113 lemma lsubf_inv_unit1: ∀g1,f2,I,K1,L2. ⦃K1.ⓤ{I}, ⫯g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
 114                        ∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓤ{I}.
 115 /2 width=5 by lsubf_inv_unit1_aux/ qed-.
 116
 117 fact lsubf_inv_atom2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ →
 118                           f1 ≗ f2 ∧ L1 = ⋆.
 119 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 120 [ /2 width=1 by conj/
 121 | #f1 #f2 #I1 #I2 #L1 #L2 #_ #H destruct
 122 | #f1 #f2 #I #L1 #L2 #_ #H destruct
 123 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
 124 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #H destruct
 125 ]
 126 qed-.
 127
 128 lemma lsubf_inv_atom2: ∀f1,f2,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ → f1 ≗ f2 ∧ L1 = ⋆.
 129 /2 width=3 by lsubf_inv_atom2_aux/ qed-.
 130
 131 fact lsubf_inv_push2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
 132                           ∀g2,I2,K2. f2 = ↑g2 → L2 = K2.ⓘ{I2} →
 133                           ∃∃g1,I1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ↑g1 & L1 = K1.ⓘ{I1}.
 134 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 135 [ #f1 #f2 #_ #g2 #J2 #K2 #_ #H destruct
 136 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J2 #K2 #H1 #H2 destruct
 137   <(injective_push … H1) -g2 /2 width=6 by ex3_3_intro/
 138 | #f1 #f2 #I #L1 #L2 #_ #g2 #J2 #K2 #H elim (discr_next_push … H)
 139 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J2 #K2 #H elim (discr_next_push … H)
 140 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J2 #K2 #H elim (discr_next_push … H)
 141 ]
 142 qed-.
 143
 144 lemma lsubf_inv_push2: ∀f1,g2,I2,L1,K2. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓘ{I2}, ↑g2⦄ →
 145                        ∃∃g1,I1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ↑g1 & L1 = K1.ⓘ{I1}.
 146 /2 width=6 by lsubf_inv_push2_aux/ qed-.
 147
 148 fact lsubf_inv_pair2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
 149                           ∀g2,I,K2,W. f2 = ⫯g2 → L2 = K2.ⓑ{I}W →
 150                           ∨∨ ∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓑ{I}W
 151                            | ∃∃g,g0,g1,K1,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
 152                                              K1 ⊢ 𝐅*⦃V⦄ ≡ g & g0 ⋓ g ≡ g1 & f1 = ⫯g1 &
 153                                              I = Abst & L1 = K1.ⓓⓝW.V.
 154 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 155 [ #f1 #f2 #_ #g2 #J #K2 #X #_ #H destruct
 156 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #X #H elim (discr_push_next … H)
 157 | #f1 #f2 #I #L1 #L2 #H12 #g2 #J #K2 #X #H1 #H2 destruct
 158   <(injective_next … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/
 159 | #f #f0 #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H12 #g2 #J #K2 #X #H1 #H2 destruct
 160   <(injective_next … H1) -g2 /3 width=10 by ex6_5_intro, or_intror/
 161 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J #K2 #X #_ #H destruct
 162 ]
 163 qed-.
 164
 165 lemma lsubf_inv_pair2: ∀f1,g2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, ⫯g2⦄ →
 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 /2 width=5 by lsubf_inv_pair2_aux/ qed-.
 171
 172 fact lsubf_inv_unit2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
 173                           ∀g2,I,K2. f2 = ⫯g2 → L2 = K2.ⓤ{I} →
 174                           ∨∨ ∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓤ{I}
 175                            | ∃∃g,g0,g1,J,K1,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
 176                                                K1 ⊢ 𝐅*⦃V⦄ ≡ g & g0 ⋓ g ≡ g1 & f1 = ⫯g1 &
 177                                                L1 = K1.ⓑ{J}V.
 178 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 179 [ #f1 #f2 #_ #g2 #J #K2 #_ #H destruct
 180 | #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #H elim (discr_push_next … H)
 181 | #f1 #f2 #I #L1 #L2 #H12 #g2 #J #K2 #H1 #H2 destruct
 182   <(injective_next … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/
 183 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #_ #H destruct
 184 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #Hf #Hf1 #H12 #g2 #J #K2 #H1 #H2 destruct
 185   <(injective_next … H1) -g2 /3 width=11 by ex5_6_intro, or_intror/
 186 ]
 187 qed-.
 188
 189 lemma lsubf_inv_unit2: ∀f1,g2,I,L1,K2. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓤ{I}, ⫯g2⦄ →
 190                        ∨∨ ∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓤ{I}
 191                         | ∃∃g,g0,g1,J,K1,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
 192                                             K1 ⊢ 𝐅*⦃V⦄ ≡ g & g0 ⋓ g ≡ g1 & f1 = ⫯g1 &
 193                                             L1 = K1.ⓑ{J}V.
 194 /2 width=5 by lsubf_inv_unit2_aux/ qed-.
 195
 196 (* Advanced inversion lemmas ************************************************)
 197
 198 lemma lsubf_inv_atom: ∀f1,f2. ⦃⋆, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ → f1 ≗ f2.
 199 #f1 #f2 #H elim (lsubf_inv_atom1 … H) -H //
 200 qed-.
 201
 202 lemma lsubf_inv_push_sn: ∀g1,f2,I1,I2,K1,K2. ⦃K1.ⓘ{I1}, ↑g1⦄ ⫃𝐅* ⦃K2.ⓘ{I2}, f2⦄ →
 203                          ∃∃g2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2.
 204 #g1 #f2 #I #K1 #K2 #X #H elim (lsubf_inv_push1 … H) -H
 205 #g2 #I #Y #H0 #H2 #H destruct /2 width=3 by ex2_intro/
 206 qed-.
 207
 208 lemma lsubf_inv_bind_sn: ∀g1,f2,I,K1,K2. ⦃K1.ⓘ{I}, ⫯g1⦄ ⫃𝐅* ⦃K2.ⓘ{I}, f2⦄ →
 209                          ∃∃g2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2.
 210 #g1 #f2 * #I [2: #X ] #K1 #K2 #H
 211 [ elim (lsubf_inv_pair1 … H) -H *
 212   [ #z2 #Y2 #H2 #H #H0 destruct /2 width=3 by ex2_intro/
 213   | #z #z0 #z2 #Y2 #W #V #_ #_ #_ #_ #H0 #_ #H destruct
 214   | #z #z0 #z2 #Z2 #Y2 #_ #_ #_ #_ #H destruct
 215   ]
 216 | elim (lsubf_inv_unit1 … H) -H
 217   #z2 #Y2 #H2 #H #H0 destruct /2 width=3 by ex2_intro/
 218 ]
 219 qed-.
 220
 221 lemma lsubf_inv_beta_sn: ∀g1,f2,K1,K2,V,W. ⦃K1.ⓓⓝW.V, ⫯g1⦄ ⫃𝐅* ⦃K2.ⓛW, f2⦄ →
 222                          ∃∃g,g0,g2. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ & K1 ⊢ 𝐅*⦃V⦄ ≡ g & g0 ⋓ g ≡ g1 & f2 = ⫯g2.
 223 #g1 #f2 #K1 #K2 #V #W #H elim (lsubf_inv_pair1 … H) -H *
 224 [ #z2 #Y2 #_ #_ #H destruct
 225 | #z #z0 #z2 #Y2 #X0 #X #H02 #Hz #Hg1 #H #_ #H0 #H1 destruct
 226   /2 width=7 by ex4_3_intro/
 227 | #z #z0 #z2 #Z2 #Y2 #_ #_ #_ #_ #H destruct
 228 ]
 229 qed-.
 230
 231 lemma lsubf_inv_unit_sn: ∀g1,f2,I,J,K1,K2,V. ⦃K1.ⓑ{I}V, ⫯g1⦄ ⫃𝐅* ⦃K2.ⓤ{J}, f2⦄ →
 232                          ∃∃g,g0,g2. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ & K1 ⊢ 𝐅*⦃V⦄ ≡ g & g0 ⋓ g ≡ g1 & f2 = ⫯g2.
 233 #g1 #f2 #I #J #K1 #K2 #V #H elim (lsubf_inv_pair1 … H) -H *
 234 [ #z2 #Y2 #_ #_ #H destruct
 235 | #z #z0 #z2 #Y2 #X0 #X #_ #_ #_ #_ #_ #_ #H destruct
 236 | #z #z0 #z2 #Z2 #Y2 #H02 #Hz #Hg1 #H0 #H1 destruct
 237   /2 width=7 by ex4_3_intro/
 238 ]
 239 qed-.
 240
 241 lemma lsubf_inv_refl: ∀L,f1,f2. ⦃L,f1⦄ ⫃𝐅* ⦃L,f2⦄ → f1 ≗ f2.
 242 #L elim L -L /2 width=1 by lsubf_inv_atom/
 243 #L #I #IH #f1 #f2 #H12
 244 elim (pn_split f1) * #g1 #H destruct
 245 [ elim (lsubf_inv_push_sn … H12) | elim (lsubf_inv_bind_sn … H12) ] -H12
 246 #g2 #H12 #H destruct /3 width=5 by eq_next, eq_push/
 247 qed-.
 248
 249 (* Basic forward lemmas *****************************************************)
 250
 251 lemma lsubf_fwd_bind_tl: ∀f1,f2,I,L1,L2.
 252                          ⦃L1.ⓘ{I}, f1⦄ ⫃𝐅* ⦃L2.ⓘ{I}, f2⦄ → ⦃L1, ⫱f1⦄ ⫃𝐅* ⦃L2, ⫱f2⦄.
 253 #f1 #f2 #I #L1 #L2 #H
 254 elim (pn_split f1) * #g1 #H0 destruct
 255 [ elim (lsubf_inv_push_sn … H) | elim (lsubf_inv_bind_sn … H) ] -H
 256 #g2 #H12 #H destruct //
 257 qed-.
 258
 259 lemma lsubf_fwd_isid_dx: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → 𝐈⦃f2⦄ → 𝐈⦃f1⦄.
 260 #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
 261 [ /2 width=3 by isid_eq_repl_fwd/
 262 | /4 width=3 by isid_inv_push, isid_push/
 263 | #f1 #f2 #I #L1 #L2 #_ #_ #H elim (isid_inv_next … H) -H //
 264 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
 265 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
 266 ]
 267 qed-.
 268
 269 lemma lsubf_fwd_isid_sn: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → 𝐈⦃f1⦄ → 𝐈⦃f2⦄.
 270 #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
 271 [ /2 width=3 by isid_eq_repl_back/
 272 | /4 width=3 by isid_inv_push, isid_push/
 273 | #f1 #f2 #I #L1 #L2 #_ #_ #H elim (isid_inv_next … H) -H //
 274 | #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
 275 | #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
 276 ]
 277 qed-.
 278
 279 lemma lsubf_fwd_sle: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → f2 ⊆ f1.
 280 #f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
 281 /3 width=5 by sor_inv_sle_sn_trans, sle_next, sle_push, sle_refl_eq, eq_sym/
 282 qed-.
 283
 284 (* Basic properties *********************************************************)
 285
 286 axiom lsubf_eq_repl_back1: ∀f2,L1,L2. eq_repl_back … (λf1. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄).
 287
 288 lemma lsubf_eq_repl_fwd1: ∀f2,L1,L2. eq_repl_fwd … (λf1. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄).
 289 #f2 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back1/
 290 qed-.
 291
 292 axiom lsubf_eq_repl_back2: ∀f1,L1,L2. eq_repl_back … (λf2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄).
 293
 294 lemma lsubf_eq_repl_fwd2: ∀f1,L1,L2. eq_repl_fwd … (λf2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄).
 295 #f1 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back2/
 296 qed-.
 297
 298 lemma lsubf_refl: bi_reflexive … lsubf.
 299 #L elim L -L /2 width=1 by lsubf_atom, eq_refl/
 300 #L #I #IH #f elim (pn_split f) * #g #H destruct
 301 /2 width=1 by lsubf_push, lsubf_bind/
 302 qed.
 303
 304 lemma lsubf_refl_eq: ∀f1,f2,L. f1 ≗ f2 → ⦃L, f1⦄ ⫃𝐅* ⦃L, f2⦄.
 305 /2 width=3 by lsubf_eq_repl_back2/ qed.
 306
 307 lemma lsubf_tl_dx: ∀g1,f2,I,L1,L2. ⦃L1, g1⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ →
 308                    ∃∃f1. ⦃L1.ⓘ{I}, f1⦄ ⫃𝐅* ⦃L2.ⓘ{I}, f2⦄ & g1 = ⫱f1.
 309 #g1 #f2 #I #L1 #L2 #H
 310 elim (pn_split f2) * #g2 #H2 destruct
 311 @ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *)
 312 qed-.
 313