-lemma csx_ind_fpbg: ∀h. ∀Q:relation3 genv lenv term.
- (∀G1,L1,T1. ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
- (∀G2,L2,T2. ⦃G1,L1,T1⦄ >[h] ⦃G2,L2,T2⦄ → Q G2 L2 T2) →
- Q G1 L1 T1
- ) →
- ∀G,L,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → Q G L T.
+lemma csx_ind_fpbg (Q:relation3 …):
+ (∀G1,L1,T1.
+ ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
+ (∀G2,L2,T2. ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → Q G2 L2 T2) →
+ Q G1 L1 T1
+ ) →
+ ∀G,L,T. ❪G,L❫ ⊢ ⬈*𝐒 T → Q G L T.