proposition: Fact bt_sg_inv x y : x⪧∅ ≈ y⪧∅ <-> x ≈ y.
proof: Proof. split; auto. rewrite bte_ext. intros H; specialize (H x). do 2 rewrite btm_inv, btm_inv_0 in H. apply proj1 in H; destruct H; try tauto; 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)