NF weak partition development: NominalAlphaRepairedBase001048Leaf2ndReflected001.

Shared variable, support, and alpha-certificate components.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy000 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy000 = NFChoice.ReplaySupport.freshVar ∅

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy001 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_001.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy001 = NFChoice.ReplaySupport.freshVar ∅ 1

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy002 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_002.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy002 = NFChoice.ReplaySupport.freshVar ∅ 2

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy003 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_003.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy004 (x y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_004.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy005 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_005.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy006 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_006.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy007 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_007.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy008 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_008.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy009 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_009.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy010 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_010.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy011 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_011.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy012 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_012.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy013 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_013.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy014 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_014.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy015 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_015.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy016 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_016.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy017 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_017.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy018 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_018.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy019 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_019.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy020 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_020.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy021 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_021.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy022 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_022.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy023 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_023.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy024 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_024.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy035 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_035.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy036 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_036.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy037 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_037.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy038 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_038.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy039 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_039.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy040 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_040.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy041 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_041.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy042 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_042.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy043 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_043.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy044 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_044.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy045 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_045.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy046 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_046.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy047 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_047.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy048 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_048.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy049 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_049.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy050 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_050.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy051 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_051.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy052 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_052.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy053 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_053.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy054 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_054.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy055 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_055.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy056 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_056.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy057 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_057.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy058 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_058.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy059 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_059.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy060 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_060.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy071 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_071.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy072 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_072.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy073 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_073.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy074 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_074.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy075 : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_075.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.alphaDummy076 (y z : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as alpha_dummy_076.

Equations

• One or more equations did not get rendered due to their size.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0000 : alphaDummy000 ∈ {alphaDummy000} ∪ {alphaDummy001} ∪ (Compiler.CompactSourceSyntax.synWex alphaDummy002 (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy000) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv alphaDummy002) (SemanticCore.Class.cv alphaDummy001)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0001 (x y z : SemanticCore.Var) : x ∈ {x} ∪ {y} ∪ (Compiler.CompactSourceSyntax.synWex z (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv z) (SemanticCore.Class.cv y)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0002 : alphaDummy001 ∈ {alphaDummy000} ∪ {alphaDummy001} ∪ (Compiler.CompactSourceSyntax.synWex alphaDummy002 (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy000) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv alphaDummy002) (SemanticCore.Class.cv alphaDummy001)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0003 (x y z : SemanticCore.Var) : y ∈ {x} ∪ {y} ∪ (Compiler.CompactSourceSyntax.synWex z (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv z) (SemanticCore.Class.cv y)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0004 : alphaDummy000 ∈ (SemanticCore.Class.cv alphaDummy000).fv ∪ (SemanticCore.Class.cv alphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0005 : alphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy005 (Compiler.CompactSourceSyntax.synWrex alphaDummy006 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy005) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy005 (Compiler.CompactSourceSyntax.synWrex alphaDummy006 (SemanticCore.Class.cv alphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0006 (x y : SemanticCore.Var) : x ∈ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0007 (x y : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy008 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy008 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0008 : alphaDummy000 ∈ (SemanticCore.Class.cab alphaDummy005 (Compiler.CompactSourceSyntax.synWrex alphaDummy006 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy005) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006))))).fv ∪ (SemanticCore.Class.cab alphaDummy005 (Compiler.CompactSourceSyntax.synWrex alphaDummy006 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy005) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0009 (x y : SemanticCore.Var) : x ∈ (SemanticCore.Class.cab (alphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy008 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y)))))).fv ∪ (SemanticCore.Class.cab (alphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy008 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0010 : alphaDummy006 ∈ (SemanticCore.Class.cv alphaDummy006).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0011 (x y : SemanticCore.Var) : alphaDummy008 x y ∈ (SemanticCore.Class.cv (alphaDummy008 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0012 : alphaDummy013 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv alphaDummy013) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv alphaDummy013) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv alphaDummy013).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0013 (x y : SemanticCore.Var) : alphaDummy015 x y ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy015 x y)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (alphaDummy015 x y)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (alphaDummy015 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0014 : alphaDummy013 ∈ (SemanticCore.Class.cv alphaDummy013).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0015 (x y : SemanticCore.Var) : alphaDummy015 x y ∈ (SemanticCore.Class.cv (alphaDummy015 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0016 : alphaDummy020 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy020) (SemanticCore.Class.cv alphaDummy021)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy020) (SemanticCore.Class.cv alphaDummy021)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0017 (x y : SemanticCore.Var) : alphaDummy023 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy023 x y)) (SemanticCore.Class.cv (alphaDummy024 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy023 x y)) (SemanticCore.Class.cv (alphaDummy024 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0018 : alphaDummy020 ∈ (SemanticCore.Class.cv alphaDummy020).fv ∪ (SemanticCore.Class.cv alphaDummy021).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0019 (x y : SemanticCore.Var) : alphaDummy023 x y ∈ (SemanticCore.Class.cv (alphaDummy023 x y)).fv ∪ (SemanticCore.Class.cv (alphaDummy024 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0020 : alphaDummy021 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy020) (SemanticCore.Class.cv alphaDummy021)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy020) (SemanticCore.Class.cv alphaDummy021)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0021 (x y : SemanticCore.Var) : alphaDummy024 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy023 x y)) (SemanticCore.Class.cv (alphaDummy024 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy023 x y)) (SemanticCore.Class.cv (alphaDummy024 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0022 : alphaDummy021 ∈ (SemanticCore.Class.cv alphaDummy020).fv ∪ (SemanticCore.Class.cv alphaDummy021).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0023 (x y : SemanticCore.Var) : alphaDummy024 x y ∈ (SemanticCore.Class.cv (alphaDummy023 x y)).fv ∪ (SemanticCore.Class.cv (alphaDummy024 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0024 : alphaDummy020 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy020)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy021)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0025 (x y : SemanticCore.Var) : alphaDummy023 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy023 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy024 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0026 : alphaDummy020 ∈ (SemanticCore.Class.cv alphaDummy020).fv ∪ (SemanticCore.Class.cv alphaDummy020).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0027 (x y : SemanticCore.Var) : alphaDummy023 x y ∈ (SemanticCore.Class.cv (alphaDummy023 x y)).fv ∪ (SemanticCore.Class.cv (alphaDummy023 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0028 : alphaDummy021 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy020)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy021)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0029 (x y : SemanticCore.Var) : alphaDummy024 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy023 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy024 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0030 : alphaDummy021 ∈ (SemanticCore.Class.cv alphaDummy021).fv ∪ (SemanticCore.Class.cv alphaDummy021).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0031 (x y : SemanticCore.Var) : alphaDummy024 x y ∈ (SemanticCore.Class.cv (alphaDummy024 x y)).fv ∪ (SemanticCore.Class.cv (alphaDummy024 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0032 : alphaDummy001 ∈ (SemanticCore.Class.cv alphaDummy000).fv ∪ (SemanticCore.Class.cv alphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0033 : alphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy005 (Compiler.CompactSourceSyntax.synWrex alphaDummy006 (SemanticCore.Class.cv alphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy005) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy005 (Compiler.CompactSourceSyntax.synWrex alphaDummy006 (SemanticCore.Class.cv alphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0034 (x y : SemanticCore.Var) : y ∈ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0035 (x y : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy008 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy008 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0036 : alphaDummy001 ∈ (SemanticCore.Class.cab alphaDummy005 (Compiler.CompactSourceSyntax.synWrex alphaDummy006 (SemanticCore.Class.cv alphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab alphaDummy005 (Compiler.CompactSourceSyntax.synWrex alphaDummy006 (SemanticCore.Class.cv alphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0037 (x y : SemanticCore.Var) : y ∈ (SemanticCore.Class.cab (alphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy008 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (alphaDummy007 x y) (Compiler.CompactSourceSyntax.synWrex (alphaDummy008 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy007 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0038 : alphaDummy006 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0039 (x y : SemanticCore.Var) : alphaDummy008 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0040 : alphaDummy006 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy006)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0041 (x y : SemanticCore.Var) : alphaDummy008 x y ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy008 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0042 : alphaDummy002 ∈ (SemanticCore.Class.cv alphaDummy002).fv ∪ (SemanticCore.Class.cv alphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0043 : alphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy041 (Compiler.CompactSourceSyntax.synWrex alphaDummy042 (SemanticCore.Class.cv alphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy041) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy041 (Compiler.CompactSourceSyntax.synWrex alphaDummy042 (SemanticCore.Class.cv alphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy041) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0044 (y z : SemanticCore.Var) : z ∈ (SemanticCore.Class.cv z).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0045 (y z : SemanticCore.Var) : z ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy043 y z) (Compiler.CompactSourceSyntax.synWrex (alphaDummy044 y z) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy043 y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy043 y z) (Compiler.CompactSourceSyntax.synWrex (alphaDummy044 y z) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy043 y z)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0046 : alphaDummy002 ∈ (SemanticCore.Class.cab alphaDummy041 (Compiler.CompactSourceSyntax.synWrex alphaDummy042 (SemanticCore.Class.cv alphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy041) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042))))).fv ∪ (SemanticCore.Class.cab alphaDummy041 (Compiler.CompactSourceSyntax.synWrex alphaDummy042 (SemanticCore.Class.cv alphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy041) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0047 (y z : SemanticCore.Var) : z ∈ (SemanticCore.Class.cab (alphaDummy043 y z) (Compiler.CompactSourceSyntax.synWrex (alphaDummy044 y z) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy043 y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z)))))).fv ∪ (SemanticCore.Class.cab (alphaDummy043 y z) (Compiler.CompactSourceSyntax.synWrex (alphaDummy044 y z) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy043 y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0048 : alphaDummy042 ∈ (SemanticCore.Class.cv alphaDummy042).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0049 (y z : SemanticCore.Var) : alphaDummy044 y z ∈ (SemanticCore.Class.cv (alphaDummy044 y z)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0050 : alphaDummy049 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv alphaDummy049) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv alphaDummy049) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv alphaDummy049).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0051 (y z : SemanticCore.Var) : alphaDummy051 y z ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (alphaDummy051 y z)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (alphaDummy051 y z)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (alphaDummy051 y z)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0052 : alphaDummy049 ∈ (SemanticCore.Class.cv alphaDummy049).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0053 (y z : SemanticCore.Var) : alphaDummy051 y z ∈ (SemanticCore.Class.cv (alphaDummy051 y z)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0054 : alphaDummy056 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy056) (SemanticCore.Class.cv alphaDummy057)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy056) (SemanticCore.Class.cv alphaDummy057)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0055 (y z : SemanticCore.Var) : alphaDummy059 y z ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy059 y z)) (SemanticCore.Class.cv (alphaDummy060 y z))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy059 y z)) (SemanticCore.Class.cv (alphaDummy060 y z))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0056 : alphaDummy056 ∈ (SemanticCore.Class.cv alphaDummy056).fv ∪ (SemanticCore.Class.cv alphaDummy057).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0057 (y z : SemanticCore.Var) : alphaDummy059 y z ∈ (SemanticCore.Class.cv (alphaDummy059 y z)).fv ∪ (SemanticCore.Class.cv (alphaDummy060 y z)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0058 : alphaDummy057 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy056) (SemanticCore.Class.cv alphaDummy057)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv alphaDummy056) (SemanticCore.Class.cv alphaDummy057)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0059 (y z : SemanticCore.Var) : alphaDummy060 y z ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy059 y z)) (SemanticCore.Class.cv (alphaDummy060 y z))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (alphaDummy059 y z)) (SemanticCore.Class.cv (alphaDummy060 y z))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0060 : alphaDummy057 ∈ (SemanticCore.Class.cv alphaDummy056).fv ∪ (SemanticCore.Class.cv alphaDummy057).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0061 (y z : SemanticCore.Var) : alphaDummy060 y z ∈ (SemanticCore.Class.cv (alphaDummy059 y z)).fv ∪ (SemanticCore.Class.cv (alphaDummy060 y z)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0062 : alphaDummy056 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy056)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy057)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0063 (y z : SemanticCore.Var) : alphaDummy059 y z ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy059 y z))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy060 y z))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0064 : alphaDummy056 ∈ (SemanticCore.Class.cv alphaDummy056).fv ∪ (SemanticCore.Class.cv alphaDummy056).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0065 (y z : SemanticCore.Var) : alphaDummy059 y z ∈ (SemanticCore.Class.cv (alphaDummy059 y z)).fv ∪ (SemanticCore.Class.cv (alphaDummy059 y z)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0066 : alphaDummy057 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy056)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv alphaDummy057)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0067 (y z : SemanticCore.Var) : alphaDummy060 y z ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy059 y z))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (alphaDummy060 y z))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0068 : alphaDummy057 ∈ (SemanticCore.Class.cv alphaDummy057).fv ∪ (SemanticCore.Class.cv alphaDummy057).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0069 (y z : SemanticCore.Var) : alphaDummy060 y z ∈ (SemanticCore.Class.cv (alphaDummy060 y z)).fv ∪ (SemanticCore.Class.cv (alphaDummy060 y z)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0070 : alphaDummy001 ∈ (SemanticCore.Class.cv alphaDummy002).fv ∪ (SemanticCore.Class.cv alphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0071 : alphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy041 (Compiler.CompactSourceSyntax.synWrex alphaDummy042 (SemanticCore.Class.cv alphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy041) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab alphaDummy041 (Compiler.CompactSourceSyntax.synWrex alphaDummy042 (SemanticCore.Class.cv alphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy041) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0072 (y z : SemanticCore.Var) : y ∈ (SemanticCore.Class.cv z).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0073 (y z : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy043 y z) (Compiler.CompactSourceSyntax.synWrex (alphaDummy044 y z) (SemanticCore.Class.cv z) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy043 y z)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (alphaDummy043 y z) (Compiler.CompactSourceSyntax.synWrex (alphaDummy044 y z) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy043 y z)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0074 : alphaDummy001 ∈ (SemanticCore.Class.cab alphaDummy041 (Compiler.CompactSourceSyntax.synWrex alphaDummy042 (SemanticCore.Class.cv alphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy041) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab alphaDummy041 (Compiler.CompactSourceSyntax.synWrex alphaDummy042 (SemanticCore.Class.cv alphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv alphaDummy041) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0075 (y z : SemanticCore.Var) : y ∈ (SemanticCore.Class.cab (alphaDummy043 y z) (Compiler.CompactSourceSyntax.synWrex (alphaDummy044 y z) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy043 y z)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (alphaDummy043 y z) (Compiler.CompactSourceSyntax.synWrex (alphaDummy044 y z) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (alphaDummy043 y z)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0076 : alphaDummy042 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0077 (y z : SemanticCore.Var) : alphaDummy044 y z ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0078 : alphaDummy042 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv alphaDummy042)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.SecondProjectionAlpha.support_mem_0079 (y z : SemanticCore.Var) : alphaDummy044 y z ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (alphaDummy044 y z))).fv