NF weak partition development: NAR4H5C094M3Part001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy000 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy000 = NFChoice.ReplaySupport.freshVar ∅

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy001 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_001.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy001 = NFChoice.ReplaySupport.freshVar ∅ 1

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy002 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_002.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy003 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_003.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy004 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_004.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy005 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_005.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy006 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_006.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy007 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_007.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy008 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_008.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy009 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_009.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy010 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_010.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy011 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_011.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy012 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_012.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy013 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_013.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy014 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_014.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy015 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_015.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy016 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_016.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy016 x y = NFChoice.ReplaySupport.freshVar ((NFChoice.SemanticCore.Class.cv x).fv ∪ (NFChoice.SemanticCore.Class.cv y).fv)

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy017 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_017.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy017 x y = NFChoice.ReplaySupport.freshVar ((NFChoice.SemanticCore.Class.cv x).fv ∪ (NFChoice.SemanticCore.Class.cv y).fv) 1

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy018 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_018.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy019 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_019.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy020 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_020.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy021 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_021.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy022 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_022.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy023 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_023.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy024 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_024.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy025 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_025.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy026 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_026.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy027 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_027.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy028 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_028.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy029 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_029.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy030 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_030.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy031 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_031.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy032 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_032.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy033 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_033.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy034 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_034.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy035 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_035.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy036 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_036.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy037 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_037.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy038 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_038.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy039 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_039.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy040 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_040.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy041 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_041.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy042 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_042.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy043 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_043.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy044 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_044.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy045 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_045.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy046 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_046.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy047 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_047.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy048 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_048.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy049 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_049.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy050 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_050.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy051 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_051.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy052 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_052.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy053 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_053.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy054 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_054.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy055 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_055.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy056 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_056.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy057 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_057.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy058 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_058.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy059 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_059.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy060 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_060.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy061 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_061.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy062 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_062.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy063 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_063.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy064 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_064.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy065 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_065.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy066 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_066.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy067 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_067.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy068 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_068.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy069 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_069.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy070 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_070.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy071 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_071.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy072 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_072.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy073 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_073.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy074 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_074.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy075 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_075.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy076 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_076.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy077 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_077.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy078 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_078.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy079 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_079.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy080 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_080.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy081 (x y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_081.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy082 : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_082.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy083 (y : SemanticCore.Var) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb094_alpha_dummy_083.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094AlphaDummy083 y = NFChoice.ReplaySupport.freshVar ((NFChoice.SemanticCore.Class.cv y).fv ∪ (NFChoice.SemanticCore.Class.cv y).fv)

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_000 : nb094AlphaDummy072 ∉ (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (SemanticCore.Class.cv nb094AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (SemanticCore.Class.cv nb094AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_001 : nb094AlphaDummy012 ∉ (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007))))).fv ∪ (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_002 (x y : SemanticCore.Var) : nb094AlphaDummy073 x y ∉ (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_003 (x y : SemanticCore.Var) : nb094AlphaDummy013 x y ∉ (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y)))))).fv ∪ (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_004 : nb094AlphaDummy020 ∉ (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015))))).fv ∪ (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_005 : nb094AlphaDummy044 ∉ (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_006 (x y : SemanticCore.Var) : nb094AlphaDummy021 x y ∉ (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y)))))).fv ∪ (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_007 (x y : SemanticCore.Var) : nb094AlphaDummy045 x y ∉ (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_008 : nb094AlphaDummy014 ∉ (SemanticCore.Class.cv nb094AlphaDummy000).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_009 : nb094AlphaDummy015 ∉ (SemanticCore.Class.cv nb094AlphaDummy000).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_010 : nb094AlphaDummy014 ≠ nb094AlphaDummy015

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_011 : nb094AlphaDummy080 ∉ (SemanticCore.Class.cv nb094AlphaDummy000).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_012 : nb094AlphaDummy082 ∉ (SemanticCore.Class.cv nb094AlphaDummy001).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_013 : nb094AlphaDummy050 ∉ (SemanticCore.Class.cv nb094AlphaDummy007).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_014 : nb094AlphaDummy051 ∉ (SemanticCore.Class.cv nb094AlphaDummy007).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_015 : nb094AlphaDummy050 ≠ nb094AlphaDummy051

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_016 (x y : SemanticCore.Var) : nb094AlphaDummy052 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy009 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_017 (x y : SemanticCore.Var) : nb094AlphaDummy053 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy009 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_018 (x y : SemanticCore.Var) : nb094AlphaDummy052 x y ≠ nb094AlphaDummy053 x y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_019 : nb094AlphaDummy022 ∉ (SemanticCore.Class.cv nb094AlphaDummy015).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_020 : nb094AlphaDummy023 ∉ (SemanticCore.Class.cv nb094AlphaDummy015).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_021 : nb094AlphaDummy022 ≠ nb094AlphaDummy023

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_022 (x y : SemanticCore.Var) : nb094AlphaDummy024 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy017 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_023 (x y : SemanticCore.Var) : nb094AlphaDummy025 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy017 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_024 (x y : SemanticCore.Var) : nb094AlphaDummy024 x y ≠ nb094AlphaDummy025 x y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_025 : nb094AlphaDummy028 ∉ (SemanticCore.Class.cv nb094AlphaDummy022).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_026 : nb094AlphaDummy029 ∉ (SemanticCore.Class.cv nb094AlphaDummy022).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_027 : nb094AlphaDummy030 ∉ (SemanticCore.Class.cv nb094AlphaDummy022).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_028 : nb094AlphaDummy028 ≠ nb094AlphaDummy029

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_029 : nb094AlphaDummy028 ≠ nb094AlphaDummy030

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_030 : nb094AlphaDummy029 ≠ nb094AlphaDummy030

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_031 (x y : SemanticCore.Var) : nb094AlphaDummy031 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy024 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_032 (x y : SemanticCore.Var) : nb094AlphaDummy032 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy024 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_033 (x y : SemanticCore.Var) : nb094AlphaDummy033 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy024 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_034 (x y : SemanticCore.Var) : nb094AlphaDummy031 x y ≠ nb094AlphaDummy032 x y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_035 (x y : SemanticCore.Var) : nb094AlphaDummy031 x y ≠ nb094AlphaDummy033 x y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_036 (x y : SemanticCore.Var) : nb094AlphaDummy032 x y ≠ nb094AlphaDummy033 x y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_037 : nb094AlphaDummy040 ∉ (SemanticCore.Class.cv nb094AlphaDummy029).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy029).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_038 : nb094AlphaDummy036 ∉ (SemanticCore.Class.cv nb094AlphaDummy029).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy030).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_039 : nb094AlphaDummy042 ∉ (SemanticCore.Class.cv nb094AlphaDummy030).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy030).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_040 (x y : SemanticCore.Var) : nb094AlphaDummy041 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy032 x y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy032 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_041 (x y : SemanticCore.Var) : nb094AlphaDummy037 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy032 x y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy033 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_042 (x y : SemanticCore.Var) : nb094AlphaDummy043 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy033 x y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy033 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_043 : nb094AlphaDummy056 ∉ (SemanticCore.Class.cv nb094AlphaDummy050).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_044 : nb094AlphaDummy057 ∉ (SemanticCore.Class.cv nb094AlphaDummy050).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_045 : nb094AlphaDummy058 ∉ (SemanticCore.Class.cv nb094AlphaDummy050).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_046 : nb094AlphaDummy056 ≠ nb094AlphaDummy057

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_047 : nb094AlphaDummy056 ≠ nb094AlphaDummy058

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_048 : nb094AlphaDummy057 ≠ nb094AlphaDummy058

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_049 (x y : SemanticCore.Var) : nb094AlphaDummy059 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy052 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_050 (x y : SemanticCore.Var) : nb094AlphaDummy060 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy052 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_051 (x y : SemanticCore.Var) : nb094AlphaDummy061 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy052 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_052 (x y : SemanticCore.Var) : nb094AlphaDummy059 x y ≠ nb094AlphaDummy060 x y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_053 (x y : SemanticCore.Var) : nb094AlphaDummy059 x y ≠ nb094AlphaDummy061 x y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_054 (x y : SemanticCore.Var) : nb094AlphaDummy060 x y ≠ nb094AlphaDummy061 x y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_055 : nb094AlphaDummy068 ∉ (SemanticCore.Class.cv nb094AlphaDummy057).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy057).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_056 : nb094AlphaDummy064 ∉ (SemanticCore.Class.cv nb094AlphaDummy057).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy058).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_057 : nb094AlphaDummy070 ∉ (SemanticCore.Class.cv nb094AlphaDummy058).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy058).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_058 (x y : SemanticCore.Var) : nb094AlphaDummy069 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy060 x y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy060 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_059 (x y : SemanticCore.Var) : nb094AlphaDummy065 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy060 x y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy061 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_060 (x y : SemanticCore.Var) : nb094AlphaDummy071 x y ∉ (SemanticCore.Class.cv (nb094AlphaDummy061 x y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy061 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_061 (x y : SemanticCore.Var) : nb094AlphaDummy016 x y ∉ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_062 (x y : SemanticCore.Var) : nb094AlphaDummy017 x y ∉ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_063 (x y : SemanticCore.Var) : nb094AlphaDummy016 x y ≠ nb094AlphaDummy017 x y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_064 (x y : SemanticCore.Var) : nb094AlphaDummy081 x y ∉ (SemanticCore.Class.cv x).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_065 (y : SemanticCore.Var) : nb094AlphaDummy083 y ∉ (SemanticCore.Class.cv y).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_066 : nb094AlphaDummy026 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy022) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb094AlphaDummy022) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy022).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_067 (x y : SemanticCore.Var) : nb094AlphaDummy027 x y ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb094AlphaDummy024 x y)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb094AlphaDummy024 x y)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy024 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_068 : nb094AlphaDummy054 ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy050) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb094AlphaDummy050) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy050).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_069 (x y : SemanticCore.Var) : nb094AlphaDummy055 x y ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb094AlphaDummy052 x y)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb094AlphaDummy052 x y)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy052 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_070 : nb094AlphaDummy010 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (SemanticCore.Class.cv nb094AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_071 (x y : SemanticCore.Var) : nb094AlphaDummy011 x y ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_072 : nb094AlphaDummy018 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_073 (x y : SemanticCore.Var) : nb094AlphaDummy019 x y ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_074 : nb094AlphaDummy038 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy029)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy030)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_075 (x y : SemanticCore.Var) : nb094AlphaDummy039 x y ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy032 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy033 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_076 : nb094AlphaDummy066 ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy057)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy058)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_077 (x y : SemanticCore.Var) : nb094AlphaDummy067 x y ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy060 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy061 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_078 : nb094AlphaDummy074 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_079 (x y : SemanticCore.Var) : nb094AlphaDummy075 x y ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_080 : nb094AlphaDummy046 ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_081 (x y : SemanticCore.Var) : nb094AlphaDummy047 x y ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_082 : nb094AlphaDummy078 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy000) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy001))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy000) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy001))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_083 : nb094AlphaDummy034 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy029) (SemanticCore.Class.cv nb094AlphaDummy030)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy029) (SemanticCore.Class.cv nb094AlphaDummy030)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_084 (x y : SemanticCore.Var) : nb094AlphaDummy035 x y ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy032 x y)) (SemanticCore.Class.cv (nb094AlphaDummy033 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy032 x y)) (SemanticCore.Class.cv (nb094AlphaDummy033 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_085 : nb094AlphaDummy062 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy057) (SemanticCore.Class.cv nb094AlphaDummy058)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy057) (SemanticCore.Class.cv nb094AlphaDummy058)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_086 (x y : SemanticCore.Var) : nb094AlphaDummy063 x y ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy060 x y)) (SemanticCore.Class.cv (nb094AlphaDummy061 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy060 x y)) (SemanticCore.Class.cv (nb094AlphaDummy061 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_087 (x y : SemanticCore.Var) : nb094AlphaDummy079 x y ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_088 : nb094AlphaDummy006 ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_089 : nb094AlphaDummy007 ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_090 : nb094AlphaDummy006 ≠ nb094AlphaDummy007

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_091 (x y : SemanticCore.Var) : nb094AlphaDummy008 x y ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy003 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_092 (x y : SemanticCore.Var) : nb094AlphaDummy009 x y ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy003 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_093 (x y : SemanticCore.Var) : nb094AlphaDummy008 x y ≠ nb094AlphaDummy009 x y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_094 : nb094AlphaDummy076 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_095 (x y : SemanticCore.Var) : nb094AlphaDummy077 x y ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_096 : nb094AlphaDummy048 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_097 (x y : SemanticCore.Var) : nb094AlphaDummy049 x y ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_098 : nb094AlphaDummy002 ∉ {nb094AlphaDummy000} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {nb094AlphaDummy001} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_099 : nb094AlphaDummy004 ∉ {nb094AlphaDummy000} ∪ {nb094AlphaDummy001} ∪ {nb094AlphaDummy002} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy000) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy001) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy002) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_100 (x y : SemanticCore.Var) : nb094AlphaDummy003 x y ∉ {x} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {y} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_101 (x y : SemanticCore.Var) : nb094AlphaDummy005 x y ∉ {x} ∪ {y} ∪ {nb094AlphaDummy003 x y} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_102 : nb094AlphaDummy000 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_fresh_103 : nb094AlphaDummy001 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_distinct_104 : nb094AlphaDummy000 ≠ nb094AlphaDummy001

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0000 : nb094AlphaDummy000 ∈ {nb094AlphaDummy000} ∪ {nb094AlphaDummy001} ∪ {nb094AlphaDummy002} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy000) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy001) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy002) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0001 (x y : SemanticCore.Var) : x ∈ {x} ∪ {y} ∪ {nb094AlphaDummy003 x y} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0002 : nb094AlphaDummy001 ∈ {nb094AlphaDummy000} ∪ {nb094AlphaDummy001} ∪ {nb094AlphaDummy002} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy000) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy001) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy002) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0003 (x y : SemanticCore.Var) : y ∈ {x} ∪ {y} ∪ {nb094AlphaDummy003 x y} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0004 : nb094AlphaDummy002 ∈ {nb094AlphaDummy000} ∪ {nb094AlphaDummy001} ∪ {nb094AlphaDummy002} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy000) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb094AlphaDummy001) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy002) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0005 (x y : SemanticCore.Var) : nb094AlphaDummy003 x y ∈ {x} ∪ {y} ∪ {nb094AlphaDummy003 x y} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0006 : nb094AlphaDummy000 ∈ {nb094AlphaDummy000} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {nb094AlphaDummy001} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0007 (x y : SemanticCore.Var) : x ∈ {x} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {y} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0008 : nb094AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0009 : nb094AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (SemanticCore.Class.cv nb094AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0010 (x y : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy003 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0011 (x y : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0012 : nb094AlphaDummy000 ∈ (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007))))).fv ∪ (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0013 (x y : SemanticCore.Var) : x ∈ (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y)))))).fv ∪ (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0014 : nb094AlphaDummy000 ∈ (SemanticCore.Class.cv nb094AlphaDummy000).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0015 : nb094AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0018 : nb094AlphaDummy000 ∈ (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015))))).fv ∪ (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0019 (x y : SemanticCore.Var) : x ∈ (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y)))))).fv ∪ (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0020 : nb094AlphaDummy015 ∈ (SemanticCore.Class.cv nb094AlphaDummy015).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0021 (x y : SemanticCore.Var) : nb094AlphaDummy017 x y ∈ (SemanticCore.Class.cv (nb094AlphaDummy017 x y)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0024 : nb094AlphaDummy022 ∈ (SemanticCore.Class.cv nb094AlphaDummy022).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0026 : nb094AlphaDummy029 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy029) (SemanticCore.Class.cv nb094AlphaDummy030)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy029) (SemanticCore.Class.cv nb094AlphaDummy030)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0027 (x y : SemanticCore.Var) : nb094AlphaDummy032 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy032 x y)) (SemanticCore.Class.cv (nb094AlphaDummy033 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy032 x y)) (SemanticCore.Class.cv (nb094AlphaDummy033 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0028 : nb094AlphaDummy029 ∈ (SemanticCore.Class.cv nb094AlphaDummy029).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy030).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0029 (x y : SemanticCore.Var) : nb094AlphaDummy032 x y ∈ (SemanticCore.Class.cv (nb094AlphaDummy032 x y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy033 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0030 : nb094AlphaDummy030 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy029) (SemanticCore.Class.cv nb094AlphaDummy030)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy029) (SemanticCore.Class.cv nb094AlphaDummy030)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0031 (x y : SemanticCore.Var) : nb094AlphaDummy033 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy032 x y)) (SemanticCore.Class.cv (nb094AlphaDummy033 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy032 x y)) (SemanticCore.Class.cv (nb094AlphaDummy033 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0032 : nb094AlphaDummy030 ∈ (SemanticCore.Class.cv nb094AlphaDummy029).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy030).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0033 (x y : SemanticCore.Var) : nb094AlphaDummy033 x y ∈ (SemanticCore.Class.cv (nb094AlphaDummy032 x y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy033 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0034 : nb094AlphaDummy029 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy029)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy030)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0035 (x y : SemanticCore.Var) : nb094AlphaDummy032 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy032 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy033 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0036 : nb094AlphaDummy029 ∈ (SemanticCore.Class.cv nb094AlphaDummy029).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy029).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0038 : nb094AlphaDummy030 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy029)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy030)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0039 (x y : SemanticCore.Var) : nb094AlphaDummy033 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy032 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy033 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0040 : nb094AlphaDummy030 ∈ (SemanticCore.Class.cv nb094AlphaDummy030).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy030).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0042 : nb094AlphaDummy001 ∈ {nb094AlphaDummy000} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {nb094AlphaDummy001} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0043 (x y : SemanticCore.Var) : y ∈ {x} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ {y} ∪ Compiler.CompactSourceSyntax.synCvv.fv ∪ (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0044 : nb094AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0045 : nb094AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (SemanticCore.Class.cv nb094AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0046 (x y : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy003 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0047 (x y : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0048 : nb094AlphaDummy001 ∈ (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007))))).fv ∪ (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0049 (x y : SemanticCore.Var) : y ∈ (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y)))))).fv ∪ (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0050 : nb094AlphaDummy001 ∈ (SemanticCore.Class.cv nb094AlphaDummy000).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0051 : nb094AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0054 : nb094AlphaDummy001 ∈ (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb094AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy015 (SemanticCore.Class.cv nb094AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy014) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0055 (x y : SemanticCore.Var) : y ∈ (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb094AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy017 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy017 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0058 : nb094AlphaDummy015 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy015)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0060 : nb094AlphaDummy007 ∈ (SemanticCore.Class.cv nb094AlphaDummy007).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0061 (x y : SemanticCore.Var) : nb094AlphaDummy009 x y ∈ (SemanticCore.Class.cv (nb094AlphaDummy009 x y)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0064 : nb094AlphaDummy050 ∈ (SemanticCore.Class.cv nb094AlphaDummy050).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0066 : nb094AlphaDummy057 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy057) (SemanticCore.Class.cv nb094AlphaDummy058)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy057) (SemanticCore.Class.cv nb094AlphaDummy058)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0067 (x y : SemanticCore.Var) : nb094AlphaDummy060 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy060 x y)) (SemanticCore.Class.cv (nb094AlphaDummy061 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy060 x y)) (SemanticCore.Class.cv (nb094AlphaDummy061 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0068 : nb094AlphaDummy057 ∈ (SemanticCore.Class.cv nb094AlphaDummy057).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy058).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0069 (x y : SemanticCore.Var) : nb094AlphaDummy060 x y ∈ (SemanticCore.Class.cv (nb094AlphaDummy060 x y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy061 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0070 : nb094AlphaDummy058 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy057) (SemanticCore.Class.cv nb094AlphaDummy058)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy057) (SemanticCore.Class.cv nb094AlphaDummy058)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0071 (x y : SemanticCore.Var) : nb094AlphaDummy061 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy060 x y)) (SemanticCore.Class.cv (nb094AlphaDummy061 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb094AlphaDummy060 x y)) (SemanticCore.Class.cv (nb094AlphaDummy061 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0072 : nb094AlphaDummy058 ∈ (SemanticCore.Class.cv nb094AlphaDummy057).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy058).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0073 (x y : SemanticCore.Var) : nb094AlphaDummy061 x y ∈ (SemanticCore.Class.cv (nb094AlphaDummy060 x y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy061 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0074 : nb094AlphaDummy057 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy057)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy058)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0075 (x y : SemanticCore.Var) : nb094AlphaDummy060 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy060 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy061 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0076 : nb094AlphaDummy057 ∈ (SemanticCore.Class.cv nb094AlphaDummy057).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy057).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0078 : nb094AlphaDummy058 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy057)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy058)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0079 (x y : SemanticCore.Var) : nb094AlphaDummy061 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy060 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb094AlphaDummy061 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0080 : nb094AlphaDummy058 ∈ (SemanticCore.Class.cv nb094AlphaDummy058).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy058).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0082 : nb094AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0083 : nb094AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb094AlphaDummy000) (SemanticCore.Class.cv nb094AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (SemanticCore.Class.cv nb094AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0084 (x y : SemanticCore.Var) : nb094AlphaDummy003 x y ∈ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv ∪ (SemanticCore.Class.cv (nb094AlphaDummy003 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0085 (x y : SemanticCore.Var) : nb094AlphaDummy003 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0086 : nb094AlphaDummy002 ∈ (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (SemanticCore.Class.cv nb094AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb094AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb094AlphaDummy007 (SemanticCore.Class.cv nb094AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb094AlphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0087 (x y : SemanticCore.Var) : nb094AlphaDummy003 x y ∈ (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb094AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb094AlphaDummy009 x y) (SemanticCore.Class.cv (nb094AlphaDummy003 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb094AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb094AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0090 : nb094AlphaDummy007 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb094AlphaDummy007)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0092 : nb094AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy000) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy001))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy000) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy001))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0093 (x y : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0094 : nb094AlphaDummy000 ∈ (SemanticCore.Class.cv nb094AlphaDummy000).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy001)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0096 : nb094AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy000) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy001))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb094AlphaDummy000) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy001))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0097 (x y : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0098 : nb094AlphaDummy001 ∈ (SemanticCore.Class.cv nb094AlphaDummy000).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb094AlphaDummy001)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb094_support_mem_0100 : nb094AlphaDummy001 ∈ (SemanticCore.Class.cv nb094AlphaDummy001).fv ∪ (SemanticCore.Class.cv nb094AlphaDummy001).fv

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