proposition: Fact hfs_pos_card n x : x ∈ hfs_card n <-> exists p, x = @hfs_pos n p.
proof: Proof. unfold hfs_pos, hfs_card. rewrite btm_repr_cls; split. + intros Hx. exists (bt2pos _ Hx). symmetry; apply bt_cls_hfs_repr_iff. rewrite bt2pos_fix; auto. + intros (p & ->). rewrite hfs_repr_bt_cls. apply pos2bt_in. Qed.
imports: List Arith Lia Max Wellfounded Setoid Eqdep_dec Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.Shared.Libs.DLW.Wf(wf_finite wf_chains) Undecidability.FOL.TRAKHTENBROT(notations fol_ops membership btree)