NF weak partition development: WPPCompactSyntaxFVExplicitPart001.

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

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_wiso (H R S A B : SemanticCore.Class) : (CompactSourceSyntax.synWiso H R S A B).fv = A.fv ∪ B.fv ∪ H.fv ∪ R.fv ∪ S.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cpprod (A B : SemanticCore.Class) : (CompactSourceSyntax.synCpprod A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_ccross : CompactSourceSyntax.synCcross.fv = ∅