Soundness of closed nominal proofs in models of the literal theory.

theorem NFChoice.ReplaySupport.valid_closed_of_nominal_proof (p : SemanticCore.Wff) (closed : p.fv = ∅) (proof : DirectNominalPrf.Nominal.NPrf p) {S : Fol.Structure Foundation.LNF} (hH : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) : SemanticCore.Wff.Valid S p

Every closed nominal proof is valid in every literal Hailperin model.