proposition: Theorem hfs_pos_n_transitive n : { l : hfs & { f : hfs -> pos (S n) & { g : pos (S n) -> hfs | hfs_transitive l /\ ∅ ∈ l /\ (forall p, g p ∈ l) /\ (forall x, x ∈ l -> exists p, x = g p) /\ (forall p, f (g p) = p) } } }.
proof: Proof. destruct (hfs_bij_t (S n)) as (u & i & j & H1 & H0 & H2 & H3 & H4). set (f x := match hfs_mem_dec x u with | left H => @j _ H | right _ => pos0 end). exists u, f, i; msplit 4; auto. + apply H0; lia. + intros x Hx. exists (j x Hx); rewrite H4; auto. + intros p; unfold f. destruct (hfs_mem_dec (i p) u) as [ H | H ]. * rewrite H3; auto. * destruct H; 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)