proposition: Fact bt_db_inv a b x y : a⪧b⪧∅ ≈ x⪧y⪧∅ <-> a ≈ x /\ b ≈ x /\ 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&H3) | [ (H1&H2) | (H1&H2) ] ]; auto. * do 2 (apply in_bte_cngr; auto). apply bte_trans with x; auto. * apply bte_trans with (1 := in_bte_comm _ _ _). do 2 (apply in_bte_cngr; 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)