(* Properties on stratified static type assignment for terms ****************)
fact snv_ssta_aux: ∀h,g,L0,T0.
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ssta h g L1 T1.
#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [||||*]
[ #k #HL0 #HT0 #_ #X #l #H2 destruct -IH3 -IH2 -IH1