proposition: Fact bt_db_inv' a b x y : a⪧b⪧∅ ≈ x⪧y⪧∅ <-> a ≈ x /\ b ≈ y \/ a ≈ y /\ b ≈ x.
proof: Proof. split. + intros H. rewrite bte_ext in H. generalize (proj1 (H a)) (proj1 (H b)) (proj2 (H x)) (proj2 (H y)). btm simpl; intros [|[|[]]] [|[|[]]] [|[|[]]] [|[|[]]]; auto. + intros [ (H1&H2) | (H1&H2) ]; auto. rewrite H1, 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)