NF weak partition development: WPPCompactSyntaxFVExplicitPart002.

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

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cdomfn : CompactSourceSyntax.synCdomfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cranfn : CompactSourceSyntax.synCranfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cmuc : CompactSourceSyntax.synCmuc.fv = ∅