proposition: Theorem bt_list_spec t : forall s, s ∈ t <-> exists s', s ≈ s' /\ s' ∊ bt_list t.
proof: Proof. induction t as [ | s t IH ] using bt_rect'. + simpl; intro; btm simpl; firstorder. + simpl; intro u; btm simpl; rewrite IH; split. * intros [ | (? & ? & ?) ]; eauto. * intros (? & ? & [<- |]); eauto. 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)