(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
+(* Advanced properties with sort-irrelevant equivalence for terms ***********)
+
+lemma fpbg_teqx_div: ∀h,G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ >[h] ❪G2,L2,T❫ →
+ ∀T2. T2 ≛ T → ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫.
+/4 width=5 by fpbg_feqx_trans, teqx_feqx, teqx_sym/ qed-.
+
(* Properties with plus-iterated structural successor for closures **********)
(* Note: this is used in the closure proof *)
-lemma fqup_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
+lemma fqup_fpbg: ∀h,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ >[h] ❪G2,L2,T2❫.
+#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
/3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_intro/
qed.