proposition: Fact bt_opair_equiv s t s' t' : ⟬s,t⟭ ≈⟬s',t'⟭ <-> s≈s' /\ t≈t'.
proof: Proof. split. 2: intros []; unfold bt_opair; auto. intros H. apply bt_db_inv' in H as [ (H1 & H2) | (H1 & H2) ]. + rewrite bt_sg_inv in H1. apply bt_db_inv' in H2 as [ (H2 & H3) | (H2 & H3) ]; auto. rewrite H3, <- H2; auto. + apply bte_sym, bt_sg_db_inv in H2 as (H3 & H4). apply bt_sg_db_inv in H1 as (H1 & H2). rewrite <- H4, <- H2; auto. Qed.
imports: List Arith Lia Max Wellfounded Setoid Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_decidable finite seteq) Undecidability.Shared.Libs.DLW.Vec(pos) Undecidability.Shared.Libs.DLW.Wf(wf_finite wf_chains) Undecidability.FOL.TRAKHTENBROT(notations fol_ops)