proposition: Fact bt_sg_db_inv a x y : a⪧∅ ≈ x⪧y⪧∅ <-> a ≈ x /\ a ≈ y.
proof: Proof. split. + intros H. rewrite bte_ext in H. generalize (proj2 (H x)) (proj2 (H y)). btm simpl; intros [|[]] [|[]]; auto. + intros []. apply bte_trans with (a⪧a⪧∅); 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)