inductive fpb (G1) (L1) (T1): relation3 genv lenv term ≝
| fpb_fqu: ∀G2,L2,T2. ❪G1,L1,T1❫ ⬂ ❪G2,L2,T2❫ → fpb G1 L1 T1 G2 L2 T2
inductive fpb (G1) (L1) (T1): relation3 genv lenv term ≝
| fpb_fqu: ∀G2,L2,T2. ❪G1,L1,T1❫ ⬂ ❪G2,L2,T2❫ → fpb G1 L1 T1 G2 L2 T2