NF weak partition development: CompactSyntaxFV.

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wtru : CompactSourceSyntax.synWtru.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wb (ph ps : SemanticCore.Wff) : (CompactSourceSyntax.synWb ph ps).fv = ph.fv ∪ ps.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wo (ph ps : SemanticCore.Wff) : (CompactSourceSyntax.synWo ph ps).fv = ph.fv ∪ ps.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wa (ph ps : SemanticCore.Wff) : (CompactSourceSyntax.synWa ph ps).fv = ph.fv ∪ ps.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_w3o (ph ps ch : SemanticCore.Wff) : (CompactSourceSyntax.synW3o ph ps ch).fv = ch.fv ∪ ph.fv ∪ ps.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_w3a (ph ps ch : SemanticCore.Wff) : (CompactSourceSyntax.synW3a ph ps ch).fv = ch.fv ∪ ph.fv ∪ ps.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wnan (ph ps : SemanticCore.Wff) : (CompactSourceSyntax.synWnan ph ps).fv = ph.fv ∪ ps.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wex (x : SemanticCore.Var) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synWex x ph).fv = ph.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wnf (x : SemanticCore.Var) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synWnf x ph).fv = ph.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wsb (y x : SemanticCore.Var) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synWsb y x ph).fv = ph.fv ∪ ph.fv.erase x ∪ {y}.erase x ∪ {x} ∪ {y}

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_weu (x : SemanticCore.Var) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synWeu x ph).fv = ph.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wmo (x : SemanticCore.Var) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synWmo x ph).fv = ph.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wnfc (x : SemanticCore.Var) (A : SemanticCore.Class) : (CompactSourceSyntax.synWnfc x A).fv = A.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wne (A B : SemanticCore.Class) : (CompactSourceSyntax.synWne A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wral (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synWral x A ph).fv = A.fv.erase x ∪ ph.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wrex (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synWrex x A ph).fv = A.fv.erase x ∪ ph.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wreu (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synWreu x A ph).fv = A.fv.erase x ∪ ph.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wrmo (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synWrmo x A ph).fv = A.fv.erase x ∪ ph.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_crab (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synCrab x A ph).fv = A.fv.erase x ∪ ph.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cvv : CompactSourceSyntax.synCvv.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wsbc (A : SemanticCore.Class) (x : SemanticCore.Var) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synWsbc A x ph).fv = A.fv ∪ ph.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_csb (A : SemanticCore.Class) (x : SemanticCore.Var) (B : SemanticCore.Class) : (CompactSourceSyntax.synCsb A x B).fv = A.fv ∪ B.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cnin (A B : SemanticCore.Class) : (CompactSourceSyntax.synCnin A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ccompl (A : SemanticCore.Class) : (CompactSourceSyntax.synCcompl A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cin (A B : SemanticCore.Class) : (CompactSourceSyntax.synCin A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cun (A B : SemanticCore.Class) : (CompactSourceSyntax.synCun A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cdif (A B : SemanticCore.Class) : (CompactSourceSyntax.synCdif A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_csymdif (A B : SemanticCore.Class) : (CompactSourceSyntax.synCsymdif A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wss (A B : SemanticCore.Class) : (CompactSourceSyntax.synWss A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wpss (A B : SemanticCore.Class) : (CompactSourceSyntax.synWpss A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_c0 : CompactSourceSyntax.synC0.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cif (ph : SemanticCore.Wff) (A B : SemanticCore.Class) : (CompactSourceSyntax.synCif ph A B).fv = A.fv ∪ B.fv ∪ ph.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cpw (A : SemanticCore.Class) : (CompactSourceSyntax.synCpw A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_csn (A : SemanticCore.Class) : (CompactSourceSyntax.synCsn A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cpr (A B : SemanticCore.Class) : (CompactSourceSyntax.synCpr A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ctp (A B C : SemanticCore.Class) : (CompactSourceSyntax.synCtp A B C).fv = A.fv ∪ B.fv ∪ C.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cuni (A : SemanticCore.Class) : (CompactSourceSyntax.synCuni A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cint (A : SemanticCore.Class) : (CompactSourceSyntax.synCint A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ciun (x : SemanticCore.Var) (A B : SemanticCore.Class) : (CompactSourceSyntax.synCiun x A B).fv = A.fv.erase x ∪ B.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_copk (A B : SemanticCore.Class) : (CompactSourceSyntax.synCopk A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_c1c : CompactSourceSyntax.synC1c.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cpw1 (A : SemanticCore.Class) : (CompactSourceSyntax.synCpw1 A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cuni1 (A : SemanticCore.Class) : (CompactSourceSyntax.synCuni1 A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cxpk (A B : SemanticCore.Class) : (CompactSourceSyntax.synCxpk A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ccnvk (A : SemanticCore.Class) : (CompactSourceSyntax.synCcnvk A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cins2k (A : SemanticCore.Class) : (CompactSourceSyntax.synCins2k A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cins3k (A : SemanticCore.Class) : (CompactSourceSyntax.synCins3k A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cimak (A B : SemanticCore.Class) : (CompactSourceSyntax.synCimak A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ccomk (A B : SemanticCore.Class) : (CompactSourceSyntax.synCcomk A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cp6 (A : SemanticCore.Class) : (CompactSourceSyntax.synCp6 A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_csik (A : SemanticCore.Class) : (CompactSourceSyntax.synCsik A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cssetk : CompactSourceSyntax.synCssetk.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cimagek (A : SemanticCore.Class) : (CompactSourceSyntax.synCimagek A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cidk : CompactSourceSyntax.synCidk.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cio (x : SemanticCore.Var) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synCio x ph).fv = ph.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_c0c : CompactSourceSyntax.synC0c.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cplc (A B : SemanticCore.Class) : (CompactSourceSyntax.synCplc A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cnnc : CompactSourceSyntax.synCnnc.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cfin : CompactSourceSyntax.synCfin.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_clefin : CompactSourceSyntax.synClefin.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cltfin : CompactSourceSyntax.synCltfin.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cncfin (A : SemanticCore.Class) : (CompactSourceSyntax.synCncfin A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ctfin (M : SemanticCore.Class) : (CompactSourceSyntax.synCtfin M).fv = M.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cevenfin : CompactSourceSyntax.synCevenfin.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_coddfin : CompactSourceSyntax.synCoddfin.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wsfin (M N : SemanticCore.Class) : (CompactSourceSyntax.synWsfin M N).fv = M.fv ∪ N.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cspfin : CompactSourceSyntax.synCspfin.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cphi (A : SemanticCore.Class) : (CompactSourceSyntax.synCphi A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cop (A B : SemanticCore.Class) : (CompactSourceSyntax.synCop A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cproj1 (A : SemanticCore.Class) : (CompactSourceSyntax.synCproj1 A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cproj2 (A : SemanticCore.Class) : (CompactSourceSyntax.synCproj2 A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_copab (x y : SemanticCore.Var) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synCopab x y ph).fv = (ph.fv.erase y).erase x ∪ ({x}.erase y).erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wbr (A R B : SemanticCore.Class) : (CompactSourceSyntax.synWbr A R B).fv = A.fv ∪ B.fv ∪ R.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_c1st : CompactSourceSyntax.synC1st.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cswap : CompactSourceSyntax.synCswap.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_csset : CompactSourceSyntax.synCsset.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ccom (A B : SemanticCore.Class) : (CompactSourceSyntax.synCcom A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cima (A B : SemanticCore.Class) : (CompactSourceSyntax.synCima A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_csi (A : SemanticCore.Class) : (CompactSourceSyntax.synCsi A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cid : CompactSourceSyntax.synCid.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cxp (A B : SemanticCore.Class) : (CompactSourceSyntax.synCxp A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ccnv (A : SemanticCore.Class) : (CompactSourceSyntax.synCcnv A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_crn (A : SemanticCore.Class) : (CompactSourceSyntax.synCrn A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cdm (A : SemanticCore.Class) : (CompactSourceSyntax.synCdm A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cres (A B : SemanticCore.Class) : (CompactSourceSyntax.synCres A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wfun (A : SemanticCore.Class) : (CompactSourceSyntax.synWfun A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wfn (A B : SemanticCore.Class) : (CompactSourceSyntax.synWfn A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wf (F A B : SemanticCore.Class) : (CompactSourceSyntax.synWf F A B).fv = A.fv ∪ B.fv ∪ F.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wf1 (F A B : SemanticCore.Class) : (CompactSourceSyntax.synWf1 F A B).fv = A.fv ∪ B.fv ∪ F.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wfo (F A B : SemanticCore.Class) : (CompactSourceSyntax.synWfo F A B).fv = A.fv ∪ B.fv ∪ F.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_wf1o (F A B : SemanticCore.Class) : (CompactSourceSyntax.synWf1o F A B).fv = A.fv ∪ B.fv ∪ F.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cfv (F A : SemanticCore.Class) : (CompactSourceSyntax.synCfv F A).fv = A.fv ∪ F.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_c2nd : CompactSourceSyntax.synC2nd.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_co (A F B : SemanticCore.Class) : (CompactSourceSyntax.synCo A F B).fv = A.fv ∪ B.fv ∪ F.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_coprab (x y z : SemanticCore.Var) (ph : SemanticCore.Wff) : (CompactSourceSyntax.synCoprab x y z ph).fv = ((ph.fv.erase z).erase y).erase x ∪ (({x}.erase z).erase y).erase x ∪ (({y}.erase z).erase y).erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cmpt (x : SemanticCore.Var) (A B : SemanticCore.Class) : (CompactSourceSyntax.synCmpt x A B).fv = A.fv.erase x ∪ B.fv.erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cmpt2 (x : SemanticCore.Var) (A : SemanticCore.Class) (y : SemanticCore.Var) (B C : SemanticCore.Class) : (CompactSourceSyntax.synCmpt2 x A y B C).fv = (A.fv.erase y).erase x ∪ (B.fv.erase y).erase x ∪ (C.fv.erase y).erase x ∪ ({x}.erase y).erase x

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ctxp (A B : SemanticCore.Class) : (CompactSourceSyntax.synCtxp A B).fv = A.fv ∪ B.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cfix (A : SemanticCore.Class) : (CompactSourceSyntax.synCfix A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ccup : CompactSourceSyntax.synCcup.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cdisj : CompactSourceSyntax.synCdisj.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_caddcfn : CompactSourceSyntax.synCaddcfn.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ccompose : CompactSourceSyntax.synCcompose.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cins2 (A : SemanticCore.Class) : (CompactSourceSyntax.synCins2 A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cins3 (A : SemanticCore.Class) : (CompactSourceSyntax.synCins3 A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cimage (A : SemanticCore.Class) : (CompactSourceSyntax.synCimage A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cins4 (A : SemanticCore.Class) : (CompactSourceSyntax.synCins4 A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_csi3 (A : SemanticCore.Class) : (CompactSourceSyntax.synCsi3 A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cfuns : CompactSourceSyntax.synCfuns.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cfns : CompactSourceSyntax.synCfns.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cpw1fn : CompactSourceSyntax.synCpw1fn.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cfullfun (F : SemanticCore.Class) : (CompactSourceSyntax.synCfullfun F).fv = F.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cclos1 (S R : SemanticCore.Class) : (CompactSourceSyntax.synCclos1 S R).fv = R.fv ∪ S.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ctrans : CompactSourceSyntax.synCtrans.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cref : CompactSourceSyntax.synCref.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cantisym : CompactSourceSyntax.synCantisym.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cpartial : CompactSourceSyntax.synCpartial.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cconnex : CompactSourceSyntax.synCconnex.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cstrict : CompactSourceSyntax.synCstrict.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cfound : CompactSourceSyntax.synCfound.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cwe : CompactSourceSyntax.synCwe.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_csym : CompactSourceSyntax.synCsym.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cer : CompactSourceSyntax.synCer.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cec (A R : SemanticCore.Class) : (CompactSourceSyntax.synCec A R).fv = A.fv ∪ R.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cqs (A R : SemanticCore.Class) : (CompactSourceSyntax.synCqs A R).fv = A.fv ∪ R.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cmap : CompactSourceSyntax.synCmap.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cen : CompactSourceSyntax.synCen.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cncs : CompactSourceSyntax.synCncs.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_clec : CompactSourceSyntax.synClec.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cltc : CompactSourceSyntax.synCltc.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cnc (A : SemanticCore.Class) : (CompactSourceSyntax.synCnc A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ctc (A : SemanticCore.Class) : (CompactSourceSyntax.synCtc A).fv = A.fv

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_c2c : CompactSourceSyntax.synC2c.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_c3c : CompactSourceSyntax.synC3c.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cce : CompactSourceSyntax.synCce.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_ctcfn : CompactSourceSyntax.synCtcfn.fv = ∅

@[simp]

theorem NFChoice.Compiler.CompactSyntaxFV.fv_syn_cspac : CompactSourceSyntax.synCspac.fv = ∅