- "strong normalization for parallel rst-transition (closure)"
- 'PRedSubTyStrong h G L T = (fsb h G L T).
+ "strong normalization for parallel rst-transition (closure)"
+ 'PRedSubTyStrong G L T = (fsb G L T).
+
+(* Basic properties *********************************************************)
+
+lemma fsb_intro (G1) (L1) (T1):
+ (∀G2,L2,T2. ❨G1,L1,T1❩ ≻ ❨G2,L2,T2❩ → ≥𝐒 ❨G2,L2,T2❩) → ≥𝐒 ❨G1,L1,T1❩.
+/5 width=1 by fpbc_intro, SN3_intro/ qed.