fact: Definition entailment_minZ phi := forall D (M : @interp sig_empty _ D) (rho : nat -> D), extensional M -> (forall sigma psi, minZ psi -> sigma ⊨ psi) -> rho ⊨ phi.
imports: Undecidability.FOL.Utils.FullSyntax List