proposition: Lemma hfs_model : forall rho, rho ⊫ HF.
proof: Proof. intros rho phi [<-|[<-|[<-|[<-|[<-|[]]]]]]; cbn. - intros x y H1 H2. apply hfs_mem_ext. intuition. - intros x. apply hfs_empty_spec. - intros x y z. apply hfs_pair_spec. - intros x y. apply hfs_union_spec. - intros x y. apply hfs_pow_spec. 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