matita/matita/contribs/lambdadelta/ground/relocation/rtmap_at.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.tcs.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/notation/relations/rat_3.ma".
  16 include "ground/arith/pnat_plus.ma".
  17 include "ground/arith/pnat_lt_pred.ma".
  18 include "ground/relocation/rtmap_id.ma".
  19
  20 (* RELOCATION MAP ***********************************************************)
  21
  22 coinductive at: relation3 rtmap pnat pnat ≝
  23 | at_refl: ∀f,g,j1,j2. ⫯f = g → 𝟏 = j1 → 𝟏 = j2 → at g j1 j2
  24 | at_push: ∀f,i1,i2. at f i1 i2 → ∀g,j1,j2. ⫯f = g → ↑i1 = j1 → ↑i2 = j2 → at g j1 j2
  25 | at_next: ∀f,i1,i2. at f i1 i2 → ∀g,j2. ↑f = g → ↑i2 = j2 → at g i1 j2
  26 .
  27
  28 interpretation "relational application (rtmap)"
  29    'RAt i1 f i2 = (at f i1 i2).
  30
  31 definition H_at_div: relation4 rtmap rtmap rtmap rtmap ≝ λf2,g2,f1,g1.
  32                      ∀jf,jg,j. @❪jf,f2❫ ≘ j → @❪jg,g2❫ ≘ j →
  33                      ∃∃j0. @❪j0,f1❫ ≘ jf & @❪j0,g1❫ ≘ jg.
  34
  35 (* Basic inversion lemmas ***************************************************)
  36
  37 lemma at_inv_ppx: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
  38 #f #i1 #i2 * -f -i1 -i2 //
  39 [ #f #i1 #i2 #_ #g #j1 #j2 #_ * #_ #x #H destruct
  40 | #f #i1 #i2 #_ #g #j2 * #_ #x #_ #H elim (discr_push_next … H)
  41 ]
  42 qed-.
  43
  44 lemma at_inv_npx: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
  45                   ∃∃j2. @❪j1,g❫ ≘ j2 & ↑j2 = i2.
  46 #f #i1 #i2 * -f -i1 -i2
  47 [ #f #g #j1 #j2 #_ * #_ #x #x1 #H destruct
  48 | #f #i1 #i2 #Hi #g #j1 #j2 * * * #x #x1 #H #Hf >(injective_push … Hf) -g destruct /2 width=3 by ex2_intro/
  49 | #f #i1 #i2 #_ #g #j2 * #_ #x #x1 #_ #H elim (discr_push_next … H)
  50 ]
  51 qed-.
  52
  53 lemma at_inv_xnx: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. ↑g = f →
  54                   ∃∃j2. @❪i1,g❫ ≘ j2 & ↑j2 = i2.
  55 #f #i1 #i2 * -f -i1 -i2
  56 [ #f #g #j1 #j2 * #_ #_ #x #H elim (discr_next_push … H)
  57 | #f #i1 #i2 #_ #g #j1 #j2 * #_ #_ #x #H elim (discr_next_push … H)
  58 | #f #i1 #i2 #Hi #g #j2 * * #x #H >(injective_next … H) -g /2 width=3 by ex2_intro/
  59 ]
  60 qed-.
  61
  62 (* Advanced inversion lemmas ************************************************)
  63
  64 alias symbol "UpArrow" (instance 3) = "successor (positive integers)".
  65 lemma at_inv_ppn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
  66                   ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
  67 #f #i1 #i2 #Hf #g #j2 #H1 #H <(at_inv_ppx … Hf … H1 H) -f -g -i1 -i2
  68 #H destruct
  69 qed-.
  70
  71 alias symbol "UpArrow" (instance 7) = "successor (positive integers)".
  72 lemma at_inv_npp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
  73                   ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
  74 #f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
  75 #x2 #Hg * -i2 #H destruct
  76 qed-.
  77
  78 lemma at_inv_npn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
  79                   ∀g,j1,j2. ↑j1 = i1 → ⫯g = f → ↑j2 = i2 → @❪j1,g❫ ≘ j2.
  80 #f #i1 #i2 #Hf #g #j1 #j2 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
  81 #x2 #Hg * -i2 #H destruct //
  82 qed-.
  83
  84 lemma at_inv_xnp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
  85                   ∀g. ↑g = f → 𝟏 = i2 → ⊥.
  86 #f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f
  87 #x2 #Hg * -i2 #H destruct
  88 qed-.
  89
  90 lemma at_inv_xnn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
  91                   ∀g,j2. ↑g = f → ↑j2 = i2 → @❪i1,g❫ ≘ j2.
  92 #f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xnx … Hf … H) -f
  93 #x2 #Hg * -i2 #H destruct //
  94 qed-.
  95
  96 lemma at_inv_pxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
  97 #f elim (pn_split … f) * /2 width=2 by ex_intro/
  98 #g #H #i1 #i2 #Hf #H1 #H2 cases (at_inv_xnp … Hf … H H2)
  99 qed-.
 100
 101 lemma at_inv_pxn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
 102                   ∃∃g. @❪i1,g❫ ≘ j2 & ↑g = f.
 103 #f elim (pn_split … f) *
 104 #g #H #i1 #i2 #Hf #j2 #H1 #H2
 105 [ elim (at_inv_ppn … Hf … H1 H H2)
 106 | /3 width=5 by at_inv_xnn, ex2_intro/
 107 ]
 108 qed-.
 109
 110 alias symbol "UpArrow" (instance 5) = "successor (positive integers)".
 111 lemma at_inv_nxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
 112                   ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
 113 #f elim (pn_split f) *
 114 #g #H #i1 #i2 #Hf #j1 #H1 #H2
 115 [ elim (at_inv_npp … Hf … H1 H H2)
 116 | elim (at_inv_xnp … Hf … H H2)
 117 ]
 118 qed-.
 119
 120 lemma at_inv_nxn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
 121                   (∃∃g. @❪j1,g❫ ≘ j2 & ⫯g = f) ∨
 122                   ∃∃g. @❪i1,g❫ ≘ j2 & ↑g = f.
 123 #f elim (pn_split f) *
 124 /4 width=7 by at_inv_xnn, at_inv_npn, ex2_intro, or_intror, or_introl/
 125 qed-.
 126
 127 (* Note: the following inversion lemmas must be checked *)
 128 lemma at_inv_xpx: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f →
 129                   ∨∨ ∧∧ 𝟏 = i1 & 𝟏 = i2
 130                    | ∃∃j1,j2. @❪j1,g❫ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
 131 #f * [2: #i1 ] #i2 #Hf #g #H
 132 [ elim (at_inv_npx … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
 133 | >(at_inv_ppx … Hf … H) -f /3 width=1 by conj, or_introl/
 134 ]
 135 qed-.
 136
 137 lemma at_inv_xpp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
 138 #f #i1 #i2 #Hf #g #H elim (at_inv_xpx … Hf … H) -f * //
 139 #j1 #j2 #_ #_ * -i2 #H destruct
 140 qed-.
 141
 142 lemma at_inv_xpn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
 143                   ∃∃j1. @❪j1,g❫ ≘ j2 & ↑j1 = i1.
 144 #f #i1 #i2 #Hf #g #j2 #H elim (at_inv_xpx … Hf … H) -f *
 145 [ #_ * -i2 #H destruct
 146 | #x1 #x2 #Hg #H1 * -i2 #H destruct /2 width=3 by ex2_intro/
 147 ]
 148 qed-.
 149
 150 lemma at_inv_xxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 𝟏 = i2 →
 151                   ∃∃g. 𝟏 = i1 & ⫯g = f.
 152 #f elim (pn_split f) *
 153 #g #H #i1 #i2 #Hf #H2
 154 [ /3 width=6 by at_inv_xpp, ex2_intro/
 155 | elim (at_inv_xnp … Hf … H H2)
 156 ]
 157 qed-.
 158
 159 lemma at_inv_xxn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀j2.  ↑j2 = i2 →
 160                   (∃∃g,j1. @❪j1,g❫ ≘ j2 & ↑j1 = i1 & ⫯g = f) ∨
 161                   ∃∃g. @❪i1,g❫ ≘ j2 & ↑g = f.
 162 #f elim (pn_split f) *
 163 #g #H #i1 #i2 #Hf #j2 #H2
 164 [ elim (at_inv_xpn … Hf … H H2) -i2 /3 width=5 by or_introl, ex3_2_intro/
 165 | lapply (at_inv_xnn … Hf … H H2) -i2 /3 width=3 by or_intror, ex2_intro/
 166 ]
 167 qed-.
 168
 169 (* Basic forward lemmas *****************************************************)
 170
 171 lemma at_increasing: ∀i2,i1,f. @❪i1,f❫ ≘ i2 → i1 ≤ i2.
 172 #i2 elim i2 -i2
 173 [ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf //
 174 | #i2 #IH * //
 175   #i1 #f #Hf elim (at_inv_nxn … Hf) -Hf [1,4: * |*: // ]
 176   /3 width=2 by ple_succ_bi, ple_succ_dx/
 177 ]
 178 qed-.
 179
 180 lemma at_increasing_strict: ∀g,i1,i2. @❪i1,g❫ ≘ i2 → ∀f. ↑f = g →
 181                             i1 < i2 ∧ @❪i1,f❫ ≘ ↓i2.
 182 #g #i1 #i2 #Hg #f #H elim (at_inv_xnx … Hg … H) -Hg -H
 183 /4 width=2 by conj, at_increasing, ple_succ_bi/
 184 qed-.
 185
 186 lemma at_fwd_id_ex: ∀f,i. @❪i,f❫ ≘ i → ∃g. ⫯g = f.
 187 #f elim (pn_split f) * /2 width=2 by ex_intro/
 188 #g #H #i #Hf elim (at_inv_xnx … Hf … H) -Hf -H
 189 #j2 #Hg #H destruct lapply (at_increasing … Hg) -Hg
 190 #H elim (plt_ge_false … H) -H //
 191 qed-.
 192
 193 (* Basic properties *********************************************************)
 194
 195 corec lemma at_eq_repl_back: ∀i1,i2. eq_repl_back (λf. @❪i1,f❫ ≘ i2).
 196 #i1 #i2 #f1 #H1 cases H1 -f1 -i1 -i2
 197 [ #f1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /2 width=2 by at_refl/
 198 | #f1 #i1 #i2 #Hf1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /3 width=7 by at_push/
 199 | #f1 #i1 #i2 #Hf1 #g1 #j2 #H #H2 #f2 #H12 cases (eq_inv_nx … H12 … H) -g1 /3 width=5 by at_next/
 200 ]
 201 qed-.
 202
 203 lemma at_eq_repl_fwd: ∀i1,i2. eq_repl_fwd (λf. @❪i1,f❫ ≘ i2).
 204 #i1 #i2 @eq_repl_sym /2 width=3 by at_eq_repl_back/
 205 qed-.
 206
 207 lemma at_le_ex: ∀j2,i2,f. @❪i2,f❫ ≘ j2 → ∀i1. i1 ≤ i2 →
 208                 ∃∃j1. @❪i1,f❫ ≘ j1 & j1 ≤ j2.
 209 #j2 elim j2 -j2 [2: #j2 #IH ] #i2 #f #Hf
 210 [ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
 211   #g [ #x2 ] #Hg [ #H2 ] #H0
 212   [ * /3 width=3 by at_refl, ex2_intro/
 213     #i1 #Hi12 destruct lapply (ple_inv_succ_bi … Hi12) -Hi12
 214     #Hi12 elim (IH … Hg … Hi12) -x2 -IH
 215     /3 width=7 by at_push, ex2_intro, ple_succ_bi/
 216   | #i1 #Hi12 elim (IH … Hg … Hi12) -IH -i2
 217     /3 width=5 by at_next, ex2_intro, ple_succ_bi/
 218   ]
 219 | elim (at_inv_xxp … Hf) -Hf //
 220   #g * -i2 #H2 #i1 #Hi12 <(ple_inv_unit_dx … Hi12)
 221   /3 width=3 by at_refl, ex2_intro/
 222 ]
 223 qed-.
 224
 225 lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @❪i2,f❫ ≘ i2 → @❪i1,f❫ ≘ i1.
 226 #i1 #i2 #H @(ple_ind_alt … H) -i1 -i2 [ #i2 | #i1 #i2 #_ #IH ]
 227 #f #Hf elim (at_fwd_id_ex … Hf) /4 width=7 by at_inv_npn, at_push, at_refl/
 228 qed-.
 229
 230 (* Main properties **********************************************************)
 231
 232 theorem at_monotonic: ∀j2,i2,f. @❪i2,f❫ ≘ j2 → ∀j1,i1. @❪i1,f❫ ≘ j1 →
 233                       i1 < i2 → j1 < j2.
 234 #j2 elim j2 -j2
 235 [ #i2 #f #H2f elim (at_inv_xxp … H2f) -H2f //
 236   #g #H21 #_ #j1 #i1 #_ #Hi elim (plt_ge_false … Hi) -Hi //
 237 | #j2 #IH #i2 #f #H2f * //
 238   #j1 #i1 #H1f #Hi elim (plt_inv_gen … Hi)
 239   #_ #Hi2 elim (at_inv_nxn … H2f (↓i2)) -H2f [1,3: * |*: // ]
 240   #g #H2g #H
 241   [ elim (at_inv_xpn … H1f … H) -f
 242     /4 width=8 by plt_inv_succ_bi, plt_succ_bi/
 243   | /4 width=8 by at_inv_xnn, plt_succ_bi/
 244   ]
 245 ]
 246 qed-.
 247
 248 theorem at_inv_monotonic: ∀j1,i1,f. @❪i1,f❫ ≘ j1 → ∀j2,i2. @❪i2,f❫ ≘ j2 →
 249                           j1 < j2 → i1 < i2.
 250 #j1 elim j1 -j1
 251 [ #i1 #f #H1f elim (at_inv_xxp … H1f) -H1f //
 252   #g * -i1 #H #j2 #i2 #H2f #Hj lapply (plt_des_gen … Hj) -Hj
 253   #H22 elim (at_inv_xpn … H2f … (↓j2) H) -f //
 254 | #j1 #IH *
 255   [ #f #H1f elim (at_inv_pxn … H1f) -H1f [ |*: // ]
 256     #g #H1g #H #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj
 257     /3 width=7 by at_inv_xnn/
 258   | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj
 259     #Hj #H22 elim (at_inv_nxn … H1f) -H1f [1,4: * |*: // ]
 260     #g #Hg #H
 261     [ elim (at_inv_xpn … H2f … (↓j2) H) -f
 262       /3 width=7 by plt_succ_bi/
 263     | /3 width=7 by at_inv_xnn/
 264     ]
 265   ]
 266 ]
 267 qed-.
 268
 269 theorem at_mono: ∀f,i,i1. @❪i,f❫ ≘ i1 → ∀i2. @❪i,f❫ ≘ i2 → i2 = i1.
 270 #f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
 271 #Hi elim (plt_ge_false i i) /3 width=6 by at_inv_monotonic, eq_sym/
 272 qed-.
 273
 274 theorem at_inj: ∀f,i1,i. @❪i1,f❫ ≘ i → ∀i2. @❪i2,f❫ ≘ i → i1 = i2.
 275 #f #i1 #i #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
 276 #Hi elim (plt_ge_false i i) /2 width=6 by at_monotonic/
 277 qed-.
 278
 279 theorem at_div_comm: ∀f2,g2,f1,g1.
 280                      H_at_div f2 g2 f1 g1 → H_at_div g2 f2 g1 f1.
 281 #f2 #g2 #f1 #g1 #IH #jg #jf #j #Hg #Hf
 282 elim (IH … Hf Hg) -IH -j /2 width=3 by ex2_intro/
 283 qed-.
 284
 285 theorem at_div_pp: ∀f2,g2,f1,g1.
 286                    H_at_div f2 g2 f1 g1 → H_at_div (⫯f2) (⫯g2) (⫯f1) (⫯g1).
 287 #f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
 288 elim (at_inv_xpx … Hf) -Hf [1,2: * |*: // ]
 289 [ #H1 #H2 destruct -IH
 290   lapply (at_inv_xpp … Hg ???) -Hg [4: |*: // ] #H destruct
 291   /3 width=3 by at_refl, ex2_intro/
 292 | #xf #i #Hf2 #H1 #H2 destruct
 293   lapply (at_inv_xpn … Hg ????) -Hg [5: * |*: // ] #xg #Hg2 #H destruct
 294   elim (IH … Hf2 Hg2) -IH -i /3 width=9 by at_push, ex2_intro/
 295 ]
 296 qed-.
 297
 298 theorem at_div_nn: ∀f2,g2,f1,g1.
 299                    H_at_div f2 g2 f1 g1 → H_at_div (↑f2) (↑g2) (f1) (g1).
 300 #f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
 301 elim (at_inv_xnx … Hf) -Hf [ |*: // ] #i #Hf2 #H destruct
 302 lapply (at_inv_xnn … Hg ????) -Hg [5: |*: // ] #Hg2
 303 elim (IH … Hf2 Hg2) -IH -i /2 width=3 by ex2_intro/
 304 qed-.
 305
 306 theorem at_div_np: ∀f2,g2,f1,g1.
 307                    H_at_div f2 g2 f1 g1 → H_at_div (↑f2) (⫯g2) (f1) (↑g1).
 308 #f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
 309 elim (at_inv_xnx … Hf) -Hf [ |*: // ] #i #Hf2 #H destruct
 310 lapply (at_inv_xpn … Hg ????) -Hg [5: * |*: // ] #xg #Hg2 #H destruct
 311 elim (IH … Hf2 Hg2) -IH -i /3 width=7 by at_next, ex2_intro/
 312 qed-.
 313
 314 theorem at_div_pn: ∀f2,g2,f1,g1.
 315                    H_at_div f2 g2 f1 g1 → H_at_div (⫯f2) (↑g2) (↑f1) (g1).
 316 /4 width=6 by at_div_np, at_div_comm/ qed-.
 317
 318 (* Properties on tls ********************************************************)
 319
 320 (* Note: this requires ↑ on first n *)
 321 lemma at_pxx_tls: ∀n,f. @❪𝟏,f❫ ≘ ↑n → @❪𝟏,⫱*[n]f❫ ≘ 𝟏.
 322 #n @(nat_ind_succ … n) -n //
 323 #n #IH #f #Hf
 324 cases (at_inv_pxn … Hf) -Hf [ |*: // ] #g #Hg #H0 destruct
 325 <tls_xn /2 width=1 by/
 326 qed.
 327
 328 (* Note: this requires ↑ on third n2 *)
 329 lemma at_tls: ∀n2,f. ⫯⫱*[↑n2]f ≡ ⫱*[n2]f → ∃i1. @❪i1,f❫ ≘ ↑n2.
 330 #n2 @(nat_ind_succ … n2) -n2
 331 [ /4 width=4 by at_eq_repl_back, at_refl, ex_intro/
 332 | #n2 #IH #f <tls_xn <tls_xn in ⊢ (??%→?); #H
 333   elim (IH … H) -IH -H #i1 #Hf
 334   elim (pn_split f) * #g #Hg destruct /3 width=8 by at_push, at_next, ex_intro/
 335 ]
 336 qed-.
 337
 338 (* Inversion lemmas with tls ************************************************)
 339
 340 (* Note: this does not require ↑ on second and third p *)
 341 lemma at_inv_nxx: ∀p,g,i1,j2. @❪↑i1,g❫ ≘ j2 → @❪𝟏,g❫ ≘ p →
 342                   ∃∃i2. @❪i1,⫱*[p]g❫ ≘ i2 & p+i2 = j2.
 343 #n elim n -n
 344 [ #g #i1 #j2 #Hg #H
 345   elim (at_inv_pxp … H) -H [ |*: // ] #f #H0
 346   elim (at_inv_npx … Hg … H0) -Hg [ |*: // ] #x2 #Hf #H2 destruct
 347   /2 width=3 by ex2_intro/
 348 | #n #IH #g #i1 #j2 #Hg #H
 349   elim (at_inv_pxn … H) -H [ |*: // ] #f #Hf2 #H0
 350   elim (at_inv_xnx … Hg … H0) -Hg #x2 #Hf1 #H2 destruct
 351   elim (IH … Hf1 Hf2) -IH -Hf1 -Hf2 #i2 #Hf #H2 destruct
 352   /2 width=3 by ex2_intro/
 353 ]
 354 qed-.
 355
 356 (* Note: this requires ↑ on first n2 *)
 357 lemma at_inv_tls: ∀n2,i1,f. @❪i1,f❫ ≘ ↑n2 → ⫯⫱*[↑n2]f ≡ ⫱*[n2]f.
 358 #n2 @(nat_ind_succ … n2) -n2
 359 [ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf // #g #H1 #H destruct
 360   /2 width=1 by eq_refl/
 361 | #n2 #IH #i1 #f #Hf
 362   elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
 363   [ #g #j1 #Hg #H1 #H2 | #g #Hg #Ho ] destruct
 364   <tls_xn /2 width=2 by/
 365 ]
 366 qed-.
 367
 368 (* Advanced inversion lemmas on isid ****************************************)
 369
 370 lemma isid_inv_at: ∀i,f. 𝐈❪f❫ → @❪i,f❫ ≘ i.
 371 #i elim i -i
 372 [ #f #H elim (isid_inv_gen … H) -H /2 width=2 by at_refl/
 373 | #i #IH #f #H elim (isid_inv_gen … H) -H /3 width=7 by at_push/
 374 ]
 375 qed.
 376
 377 lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈❪f❫ → @❪i1,f❫ ≘ i2 → i1 = i2.
 378 /3 width=6 by isid_inv_at, at_mono/ qed-.
 379
 380 (* Advanced properties on isid **********************************************)
 381
 382 corec lemma isid_at: ∀f. (∀i. @❪i,f❫ ≘ i) → 𝐈❪f❫.
 383 #f #Hf lapply (Hf (𝟏))
 384 #H cases (at_fwd_id_ex … H) -H
 385 #g #H @(isid_push … H) /3 width=7 by at_inv_npn/
 386 qed-.
 387
 388 (* Advanced properties on id ************************************************)
 389
 390 lemma id_inv_at: ∀f. (∀i. @❪i,f❫ ≘ i) → 𝐈𝐝 ≡ f.
 391 /3 width=1 by isid_at, eq_id_inv_isid/ qed-.
 392
 393 lemma id_at: ∀i. @❪i,𝐈𝐝❫ ≘ i.
 394 /2 width=1 by isid_inv_at/ qed.
 395
 396 (* Advanced forward lemmas on id ********************************************)
 397
 398 lemma at_id_fwd: ∀i1,i2. @❪i1,𝐈𝐝❫ ≘ i2 → i1 = i2.
 399 /2 width=4 by at_mono/ qed.
 400
 401 (* Main properties on id ****************************************************)
 402
 403 theorem at_div_id_dx: ∀f. H_at_div f 𝐈𝐝 𝐈𝐝 f.
 404 #f #jf #j0 #j #Hf #H0
 405 lapply (at_id_fwd … H0) -H0 #H destruct
 406 /2 width=3 by ex2_intro/
 407 qed-.
 408
 409 theorem at_div_id_sn: ∀f. H_at_div 𝐈𝐝 f f 𝐈𝐝.
 410 /3 width=6 by at_div_id_dx, at_div_comm/ qed-.