proposition: Fact bt_mcomp_spec x t u : u ∈ bt_mcomp x t <-> exists k, k ∈ t /\ u ≈ x⪧k.
proof: Proof. revert u; induction t as [ | s t Ht ] using bt_rect'; intros u; simpl. + rewrite btm_inv_0; split; try tauto. intros (k & Hk & _); revert Hk; rewrite btm_inv_0; auto. + rewrite btm_inv; split. * intros [ H | H ]. - exists s; split; auto; btm simpl. - rewrite Ht in H. destruct H as (k & ? & ?). exists k; split; auto. btm simpl. * intros (k & H1 & H2); revert H1 H2. rewrite btm_inv, Ht. intros [H2|H2] H1; auto. - left; apply bte_trans with (1 := H1); auto. - right; exists k; 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)