inductive ysc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
| ysc_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ysc h g G1 L1 T1 G2 L2 T2
| ysc_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g G1 L1 T1 G1 L1 T2
-| ysc_ssta : â\88\80T2,l. â¦\83G1, L1â¦\84 â\8a¢ T1 â\80¢[h, g] â¦\83l+1, T2â¦\84 → ysc h g G1 L1 T1 G1 L1 T2
+| ysc_ssta : â\88\80T2,l. â¦\83G1, L1â¦\84 â\8a¢ T1 â\96ª[h, g] l+1 â\86\92 â¦\83G1, L1â¦\84 â\8a¢ T1 â\80¢[h, g] T2 → ysc h g G1 L1 T1 G1 L1 T2
| ysc_lsubsv: ∀L2. G1 ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) → ysc h g G1 L1 T1 G1 L2 T1
.
(* Inversion lemmas on "big tree" parallel reduction for closures ***********)
lemma ypr_inv_ysc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨
+ ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨
∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡ L2 & T1 = T2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /3 width=1/ /3 width=2/
[ #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct /3 width=1/ /4 width=1/