proposition: Lemma HFN_model : exists V (M : interp V), extensional M /\ standard M /\ forall rho, rho ⊫ HFN.
proof: Proof. exists hfs, hfs_interp. split; try reflexivity. split. - intros x Hx. destruct (hfs_model_standard Hx) as [n Hn]. now exists n. - intros rho phi [<-|H]; try now apply hfs_model. cbn. intros x H. apply (@HFN_model' x). split; try apply H. intros y Hy % H. enough (hfs_cons y y = hfs_union (hfs_pair y (hfs_pair y y))) as -> by trivial. apply hfs_mem_ext. setoid_rewrite hfs_cons_spec. setoid_rewrite hfs_union_spec. intros z; split; intros Hz. + destruct Hz as [->|Hz]. * exists (hfs_pair y y). rewrite !hfs_pair_spec. tauto. * exists y. rewrite hfs_pair_spec. tauto. + destruct Hz as [u[[->| ->] % hfs_pair_spec Hu]]; auto. left. apply hfs_pair_spec in Hu. tauto. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts) Undecidability.FOL(Sets.ZF) Undecidability.FOL(ZF) Undecidability.FOL.TRAKHTENBROT(hfs) Undecidability.Shared.Libs.DLW.Utils(finite) Undecidability(Shared.ListAutomation) Lia