proposition: Lemma bti_norm_incl s t : s ⊆ t <-> map bt_norm (bt_list s) ⊑ map bt_norm (bt_list t).
proof: Proof. split. + intros H ?; rewrite !in_map_iff. intros (x & <- & Hx). specialize (H x); spec in H. { apply bt_list_spec; exists x; auto. } apply bt_list_spec in H as (y & ? & ?). exists y; split; auto. apply bte_norm_iff; auto. + intros H x Hx. apply bt_list_spec in Hx as (y & H1 & H2). apply in_map with (f := bt_norm), H, in_map_iff in H2 as (z & H3 & H2). apply bt_list_spec; exists z; split; auto. apply bte_norm_iff in H3; 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)