NF weak partition development: WPPCompactSyntaxFVExplicitPart003.

Explicit-only FV equations for the WPP extension; no global simp attributes.

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfrec (F I : SemanticCore.Class) : (CompactSourceSyntax.synCfrec F I).fv = F.fv ∪ I.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_wwpp : CompactSourceSyntax.synWwpp.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cqkrel (A : SemanticCore.Class) : (CompactSourceSyntax.synCqkrel A).fv = A.fv