definition fpbqa: ∀h. sd h → tri_relation genv lenv term ≝
λh,g,G1,L1,T1,G2,L2,T2.
⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄.
definition fpbqa: ∀h. sd h → tri_relation genv lenv term ≝
λh,g,G1,L1,T1,G2,L2,T2.
⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨ ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄.