Freshness descends through nominal class substitution.

theorem NFChoice.ReplaySupport.not_mem_support_union (v : SemanticCore.Var) (left right : Finset SemanticCore.Var) (hleft : v ∉ left) (hright : v ∉ right) : v ∉ left ∪ right

theorem NFChoice.ReplaySupport.not_mem_class_variable (a b : SemanticCore.Var) (h : a ≠ b) : a ∉ (SemanticCore.Class.cv b).fv

theorem NFChoice.ReplaySupport.not_mem_syn_wsbc (v : SemanticCore.Var) (A : SemanticCore.Class) (x : SemanticCore.Var) (ph : SemanticCore.Wff) (hA : v ∉ A.fv) (hph : v ∉ ph.fv) : v ∉ (Compiler.CompactSourceSyntax.synWsbc A x ph).fv