1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/dynamic/snv_cpcs.ma".
17 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
19 (* Properties on stratified static type assignment for terms ****************)
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]
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
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/