fact aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term.
(∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
(∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
fact aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term.
(∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
(∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →