(**************************************************************************)
include "basic_2/notation/relations/btpredstarproper_8.ma".
-include "basic_2/substitution/fqup.ma".
include "basic_2/reduction/fpbc.ma".
include "basic_2/computation/fpbs.ma".
⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2
lapply (fpbg_fwd_fpbs … H1) #H0
-elim (fpb_fpbc_or_refl … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ]
+elim (fpb_fpbc_or_fpn … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ]
/2 width=5 by fpbg_inj, fpbg_step/
qed-.