-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 (h) (Q:relation3 …):
+ (∀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.