proposition: Fact btm_inv u s t : u ∈ s⪧t <-> u ≈ s \/ u ∈ t.
proof: Proof. split. + intros H. apply bte_rincl with (u := u) in H as (v & H & ?); auto. inv btri H. right; apply bte_trans with (v⪧t); auto. apply btrm_btm; auto. + intros []. * apply btm_congr_l with s; auto. * apply bte_trans with (1 := in_bte_comm _ _ _); 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)