matita/matita/contribs/lambdadelta/basic_2/static/lsuba_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 "basic_2/relocation/drops.ma".
  16 include "basic_2/static/lsuba.ma".
  17
  18 (* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************)
  19
  20 (* Properties with generic slicing for local environments *******************)
  21
  22 (* Note: the premise 𝐔⦃f⦄ cannot be removed *)
  23 (* Basic_2A1: includes: lsuba_drop_O1_conf *)
  24 lemma lsuba_drops_conf_isuni: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 →
  25                               ∀b,f,K1. 𝐔⦃f⦄ → ⬇*[b, f] L1 ≘ K1 →
  26                               ∃∃K2. G ⊢ K1 ⫃⁝ K2 & ⬇*[b, f] L2 ≘ K2.
  27 #G #L1 #L2 #H elim H -L1 -L2
  28 [ /2 width=3 by ex2_intro/
  29 | #I #L1 #L2 #HL12 #IH #b #f #K1 #Hf #H
  30   elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
  31   [ #Hf #H destruct -IH
  32     /3 width=3 by lsuba_bind, drops_refl, ex2_intro/
  33   | #g #Hg #HLK1 #H destruct -HL12
  34     elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
  35   ]
  36 | #L1 #L2 #W #V #A #HV #HW #HL12 #IH #b #f #K1 #Hf #H
  37   elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
  38   [ #Hf #H destruct -IH
  39     /3 width=3 by drops_refl, lsuba_beta, ex2_intro/
  40   | #g #Hg #HLK1 #H destruct -HL12
  41     elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
  42   ]
  43 ]
  44 qed-.
  45
  46 (* Note: the premise 𝐔⦃f⦄ cannot be removed *)
  47 (* Basic_2A1: includes: lsuba_drop_O1_trans *)
  48 lemma lsuba_drops_trans_isuni: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 →
  49                                ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b, f] L2 ≘ K2 →
  50                                ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⬇*[b, f] L1 ≘ K1.
  51 #G #L1 #L2 #H elim H -L1 -L2
  52 [ /2 width=3 by ex2_intro/
  53 | #I #L1 #L2 #HL12 #IH #b #f #K2 #Hf #H
  54   elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
  55   [ #Hf #H destruct -IH
  56     /3 width=3 by lsuba_bind, drops_refl, ex2_intro/
  57   | #g #Hg #HLK2 #H destruct -HL12
  58     elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
  59   ]
  60 | #L1 #L2 #W #V #A #HV #HW #HL12 #IH #b #f #K2 #Hf #H
  61   elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
  62   [ #Hf #H destruct -IH
  63     /3 width=3 by drops_refl, lsuba_beta, ex2_intro/
  64   | #g #Hg #HLK2 #H destruct -HL12
  65     elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
  66   ]
  67 ]
  68 qed-.