matita/matita/contribs/lambdadelta/ground/relocation/rtmap_after_nat_uni.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/relocation/rtmap_uni.ma".
  16 include "ground/relocation/rtmap_nat.ma".
  17 include "ground/relocation/rtmap_after.ma".
  18
  19 (* RELOCATION MAP ***********************************************************)
  20
  21 lemma after_uni_dx: ∀l2,l1,f2. @↑❪l1, f2❫ ≘ l2 →
  22                     ∀f. f2 ⊚ 𝐔❨l1❩ ≘ f → 𝐔❨l2❩ ⊚ ⫱*[l2] f2 ≘ f.
  23 #l2 @(nat_ind_succ … l2) -l2
  24 [ #l1 #f2 #Hf2 #f #Hf
  25   elim (rm_nat_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
  26   lapply (after_isid_inv_dx … Hf ?) -Hf
  27   /3 width=3 by after_isid_sn, after_eq_repl_back0/
  28 | #l2 #IH #l1 #f2 #Hf2 #f #Hf
  29   elim (rm_nat_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
  30   [ #g2 #k1 #Hg2 #H1 #H2 destruct
  31     elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
  32     <tls_xn /3 width=5 by after_next/
  33   | #g2 #Hg2 #H2 destruct
  34     elim (after_inv_nxx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
  35     <tls_xn /3 width=5 by after_next/
  36   ]
  37 ]
  38 qed.
  39
  40 lemma after_uni_sn: ∀l2,l1,f2. @↑❪l1, f2❫ ≘ l2 →
  41                     ∀f. 𝐔❨l2❩ ⊚ ⫱*[l2] f2 ≘ f → f2 ⊚ 𝐔❨l1❩ ≘ f.
  42 #l2 @(nat_ind_succ … l2) -l2
  43 [ #l1 #f2 #Hf2 #f #Hf
  44   elim (rm_nat_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
  45   lapply (after_isid_inv_sn … Hf ?) -Hf
  46   /3 width=3 by after_isid_dx, after_eq_repl_back0/
  47 | #l2 #IH #l1 #f2 #Hf2 #f #Hf
  48   elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
  49   elim (rm_nat_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
  50   [ #g2 #k1 #Hg2 #H1 #H2 destruct /3 width=7 by after_push/
  51   | #g2 #Hg2 #H2 destruct /3 width=5 by after_next/
  52   ]
  53 ]
  54 qed-.
  55