matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.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/dynamic/snv_cpcs.ma".
  16
  17 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
  18
  19 (* Properties on stratified static type assignment for terms ****************)
  20
  21 fact snv_ssta_aux: ∀h,g,L,T. (
  22                       ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] →
  23                       ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 →
  24                       ♯{L0, T0} < ♯{L, T} → ⦃h, L0⦄ ⊩ U0 :[g]
  25                    ) →
  26                    ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] →
  27                    ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 →
  28                    L0 = L → T0 = T → ⦃h, L0⦄ ⊩ U0 :[g].
  29 #h #g #L #T #IH1 #L0 #T0 * -L0 -T0
  30 [
  31 |
  32 |
  33 | #a #L0 #V #W #W0 #T0 #V0 #l0 #HV #HT0 #HVW #HW0 #HTV0 #X #l #H #H1 #H2 destruct
  34   elim (ssta_inv_appl1 … H) -H #U0 #HTU0 #H destruct
  35   lapply (IH1 … HT0 … HTU0 ?) // #HU0
  36   @(snv_appl … HV HU0 HVW HW0) -HV -HU0 -HVW -HW0
  37 | #L0 #W #T0 #W0 #l0 #_ #HT0 #_ #_ #U0 #l #H #H1 #H2 destruct -W0
  38   lapply (ssta_inv_cast1 … H) -H /2 width=5/