proposition: Fact hfs_bij_t n : { t : hfs & { f : pos n -> hfs & { g : forall x, x ∈ t -> pos n | hfs_transitive t /\ (0 < n -> ∅ ∈ t) /\ (forall p, f p ∈ t) /\ (forall p H, g (f p) H = p) /\ forall x H, f (g x H) = x } } }.
proof: Proof. exists (hfs_card n), (@hfs_pos _), (@hfs_card_pos _); msplit 4. + apply hfs_card_transitive. + destruct n as [ | n ]; try lia; intros _; apply hfs_card_empty. + apply hfs_pos_prop. + intros p H; apply hfs_pos_inj; rewrite <- hfs_card_pos_spec; auto. + intros; rewrite <- hfs_card_pos_spec; auto. 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)