Nominal proof certificates grouped in dependency order.

Certificates from NAR4C084C001Part001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy000 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy000 A B R = NFChoice.ReplaySupport.freshVar (R.fv ∪ A.fv ∪ B.fv)

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy001 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_001.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy001 A B R = NFChoice.ReplaySupport.freshVar (R.fv ∪ A.fv ∪ B.fv) 1

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy002 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_002.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy002 A B R = NFChoice.ReplaySupport.freshVar (R.fv ∪ A.fv ∪ B.fv) 2

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy003 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_003.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy004 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_004.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy005 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_005.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy006 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_006.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy007 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_007.

Equations

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

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

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_008.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy009 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_009.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy010 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_010.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy011 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_011.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy012 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_012.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy013 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_013.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy014 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_014.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy015 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_015.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy016 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_016.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy017 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_017.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy018 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_018.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy019 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_019.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy020 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_020.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy021 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_021.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy022 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_022.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy023 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_023.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy024 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_024.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy025 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_025.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy026 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_026.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy027 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_027.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy028 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_028.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy029 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_029.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy030 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_030.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy031 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_031.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy032 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_032.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy033 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_033.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy034 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_034.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy035 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_035.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy036 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_036.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy037 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_037.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy038 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_038.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy039 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_039.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy040 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_040.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy041 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_041.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy042 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_042.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy043 (A B R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_043.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084AlphaDummy044 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : SemanticCore.Var

Checked nominal proof certificate identified upstream as nb084_alpha_dummy_044.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_000 (A B R : SemanticCore.Class) : nb084AlphaDummy015 A B R ∉ (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R)))))).fv ∪ (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_001 (A B R : SemanticCore.Class) : nb084AlphaDummy039 A B R ∉ (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy004 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy004 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_002 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy016 x y A R ∉ (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R)))))).fv ∪ (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_003 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy040 x y A R ∉ (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_004 (A B R : SemanticCore.Class) : nb084AlphaDummy007 A B R ∉ (SemanticCore.Class.cv (nb084AlphaDummy001 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy002 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_005 (A B R : SemanticCore.Class) : nb084AlphaDummy009 A B R ∉ (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy004 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_006 (A B R : SemanticCore.Class) : nb084AlphaDummy010 A B R ∉ (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy004 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_007 (A B R : SemanticCore.Class) : nb084AlphaDummy009 A B R ≠ nb084AlphaDummy010 A B R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_008 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy011 x y A R ∉ (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_009 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy012 x y A R ∉ (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_010 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy011 x y A R ≠ nb084AlphaDummy012 x y A R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_011 (A B R : SemanticCore.Class) : nb084AlphaDummy017 A B R ∉ (SemanticCore.Class.cv (nb084AlphaDummy010 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_012 (A B R : SemanticCore.Class) : nb084AlphaDummy018 A B R ∉ (SemanticCore.Class.cv (nb084AlphaDummy010 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_013 (A B R : SemanticCore.Class) : nb084AlphaDummy017 A B R ≠ nb084AlphaDummy018 A B R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_014 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy019 x y A R ∉ (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_015 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy020 x y A R ∉ (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_016 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy019 x y A R ≠ nb084AlphaDummy020 x y A R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_017 (A B R : SemanticCore.Class) : nb084AlphaDummy023 A B R ∉ (SemanticCore.Class.cv (nb084AlphaDummy017 A B R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_018 (A B R : SemanticCore.Class) : nb084AlphaDummy024 A B R ∉ (SemanticCore.Class.cv (nb084AlphaDummy017 A B R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_019 (A B R : SemanticCore.Class) : nb084AlphaDummy025 A B R ∉ (SemanticCore.Class.cv (nb084AlphaDummy017 A B R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_020 (A B R : SemanticCore.Class) : nb084AlphaDummy023 A B R ≠ nb084AlphaDummy024 A B R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_021 (A B R : SemanticCore.Class) : nb084AlphaDummy023 A B R ≠ nb084AlphaDummy025 A B R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_022 (A B R : SemanticCore.Class) : nb084AlphaDummy024 A B R ≠ nb084AlphaDummy025 A B R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_023 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy026 x y A R ∉ (SemanticCore.Class.cv (nb084AlphaDummy019 x y A R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_024 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy027 x y A R ∉ (SemanticCore.Class.cv (nb084AlphaDummy019 x y A R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_025 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy028 x y A R ∉ (SemanticCore.Class.cv (nb084AlphaDummy019 x y A R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_026 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy026 x y A R ≠ nb084AlphaDummy027 x y A R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_027 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy026 x y A R ≠ nb084AlphaDummy028 x y A R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_028 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy027 x y A R ≠ nb084AlphaDummy028 x y A R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_029 (A B R : SemanticCore.Class) : nb084AlphaDummy035 A B R ∉ (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_030 (A B R : SemanticCore.Class) : nb084AlphaDummy031 A B R ∉ (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy025 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_031 (A B R : SemanticCore.Class) : nb084AlphaDummy037 A B R ∉ (SemanticCore.Class.cv (nb084AlphaDummy025 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy025 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_032 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy036 x y A R ∉ (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_033 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy032 x y A R ∉ (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_034 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy038 x y A R ∉ (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_036 (A B R : SemanticCore.Class) : nb084AlphaDummy021 A B R ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb084AlphaDummy017 A B R)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb084AlphaDummy017 A B R)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy017 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_037 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy022 x y A R ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb084AlphaDummy019 x y A R)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb084AlphaDummy019 x y A R)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy019 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_038 (A B R : SemanticCore.Class) : nb084AlphaDummy013 A B R ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy004 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_039 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy014 x y A R ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_040 (A B R : SemanticCore.Class) : nb084AlphaDummy033 A B R ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy024 A B R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy025 A B R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_041 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy034 x y A R ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_042 (A B R : SemanticCore.Class) : nb084AlphaDummy041 A B R ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_043 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy042 x y A R ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_044 (A B R : SemanticCore.Class) : nb084AlphaDummy029 A B R ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)) (SemanticCore.Class.cv (nb084AlphaDummy025 A B R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)) (SemanticCore.Class.cv (nb084AlphaDummy025 A B R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_045 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy030 x y A R ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)) (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)) (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_046 (A B R : SemanticCore.Class) : nb084AlphaDummy043 A B R ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_047 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy044 x y A R ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_048 (A B R : SemanticCore.Class) : nb084AlphaDummy003 A B R ∉ R.fv ∪ A.fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy001 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy002 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_049 (A B R : SemanticCore.Class) : nb084AlphaDummy004 A B R ∉ R.fv ∪ A.fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy001 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy002 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_050 (A B R : SemanticCore.Class) : nb084AlphaDummy003 A B R ≠ nb084AlphaDummy004 A B R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_051 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy005 x y A R ∉ R.fv ∪ A.fv ∪ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_052 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy006 x y A R ∉ R.fv ∪ A.fv ∪ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_053 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy005 x y A R ≠ nb084AlphaDummy006 x y A R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_054 (A B R : SemanticCore.Class) : nb084AlphaDummy000 A B R ∉ R.fv ∪ A.fv ∪ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_055 (A B R : SemanticCore.Class) : nb084AlphaDummy001 A B R ∉ R.fv ∪ A.fv ∪ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_fresh_056 (A B R : SemanticCore.Class) : nb084AlphaDummy002 A B R ∉ R.fv ∪ A.fv ∪ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_057 (A B R : SemanticCore.Class) : nb084AlphaDummy000 A B R ≠ nb084AlphaDummy001 A B R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_058 (A B R : SemanticCore.Class) : nb084AlphaDummy000 A B R ≠ nb084AlphaDummy002 A B R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_distinct_059 (A B R : SemanticCore.Class) : nb084AlphaDummy001 A B R ≠ nb084AlphaDummy002 A B R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0000 (A B R : SemanticCore.Class) : nb084AlphaDummy001 A B R ∈ R.fv ∪ A.fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy001 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy002 A B R)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0002 (A B R : SemanticCore.Class) : nb084AlphaDummy001 A B R ∈ (SemanticCore.Class.cv (nb084AlphaDummy001 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy002 A B R)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0004 (A B R : SemanticCore.Class) : nb084AlphaDummy002 A B R ∈ R.fv ∪ A.fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy001 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy002 A B R)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0006 (A B R : SemanticCore.Class) : nb084AlphaDummy002 A B R ∈ (SemanticCore.Class.cv (nb084AlphaDummy001 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy002 A B R)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0008 (A B R : SemanticCore.Class) : nb084AlphaDummy003 A B R ∈ (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy004 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0009 (A B R : SemanticCore.Class) : nb084AlphaDummy003 A B R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy004 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0010 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy005 x y A R ∈ (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0011 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy005 x y A R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0012 (A B R : SemanticCore.Class) : nb084AlphaDummy003 A B R ∈ (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R)))))).fv ∪ (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0013 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy005 x y A R ∈ (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R)))))).fv ∪ (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0014 (A B R : SemanticCore.Class) : nb084AlphaDummy010 A B R ∈ (SemanticCore.Class.cv (nb084AlphaDummy010 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0015 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy012 x y A R ∈ (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0016 (A B R : SemanticCore.Class) : nb084AlphaDummy017 A B R ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb084AlphaDummy017 A B R)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb084AlphaDummy017 A B R)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy017 A B R)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0018 (A B R : SemanticCore.Class) : nb084AlphaDummy017 A B R ∈ (SemanticCore.Class.cv (nb084AlphaDummy017 A B R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0019 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy019 x y A R ∈ (SemanticCore.Class.cv (nb084AlphaDummy019 x y A R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0020 (A B R : SemanticCore.Class) : nb084AlphaDummy024 A B R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)) (SemanticCore.Class.cv (nb084AlphaDummy025 A B R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)) (SemanticCore.Class.cv (nb084AlphaDummy025 A B R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0021 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy027 x y A R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)) (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)) (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0022 (A B R : SemanticCore.Class) : nb084AlphaDummy024 A B R ∈ (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy025 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0023 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy027 x y A R ∈ (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0024 (A B R : SemanticCore.Class) : nb084AlphaDummy025 A B R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)) (SemanticCore.Class.cv (nb084AlphaDummy025 A B R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)) (SemanticCore.Class.cv (nb084AlphaDummy025 A B R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0025 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy028 x y A R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)) (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)) (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0026 (A B R : SemanticCore.Class) : nb084AlphaDummy025 A B R ∈ (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy025 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0027 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy028 x y A R ∈ (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0028 (A B R : SemanticCore.Class) : nb084AlphaDummy024 A B R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy024 A B R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy025 A B R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0029 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy027 x y A R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0030 (A B R : SemanticCore.Class) : nb084AlphaDummy024 A B R ∈ (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy024 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0031 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy027 x y A R ∈ (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0032 (A B R : SemanticCore.Class) : nb084AlphaDummy025 A B R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy024 A B R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy025 A B R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0033 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy028 x y A R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy027 x y A R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0034 (A B R : SemanticCore.Class) : nb084AlphaDummy025 A B R ∈ (SemanticCore.Class.cv (nb084AlphaDummy025 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy025 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0035 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy028 x y A R ∈ (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy028 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0036 (A B R : SemanticCore.Class) : nb084AlphaDummy004 A B R ∈ (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy004 A B R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0037 (A B R : SemanticCore.Class) : nb084AlphaDummy004 A B R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy004 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0038 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy006 x y A R ∈ (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)).fv ∪ (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0039 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy006 x y A R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0040 (A B R : SemanticCore.Class) : nb084AlphaDummy004 A B R ∈ (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy004 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy004 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0041 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy006 x y A R ∈ (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy006 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0042 (A B R : SemanticCore.Class) : nb084AlphaDummy010 A B R ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0043 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy012 x y A R ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0044 (A B R : SemanticCore.Class) : nb084AlphaDummy010 A B R ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))).fv

Certificates from NAR4C084C001Part002.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_support_mem_0045 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy012 x y A R ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0000 (A B R : SemanticCore.Class) : nb084AlphaDummy000 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_compact_envfresh_0000 (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) : Nominal.TEnvFresh [(nb084AlphaDummy000 A B R, d)] A.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0000 (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) : Nominal.TReflOn [(nb084AlphaDummy000 A B R, d)] A.fv

Checked nominal proof certificate identified upstream as nb084_focused_refl_0000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0000 A B R d dv_A_d = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0001 (A B R : SemanticCore.Class) : nb084AlphaDummy001 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0002 (A B R : SemanticCore.Class) : nb084AlphaDummy000 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_compact_envfresh_0001 (x : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_B_d : d ∉ B.fv) (dv_B_x : x ∉ B.fv) : Nominal.TEnvFresh [(nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)] B.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0001 (x : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_B_d : d ∉ B.fv) (dv_B_x : x ∉ B.fv) : Nominal.TReflOn [(nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)] B.fv

Checked nominal proof certificate identified upstream as nb084_focused_refl_0001.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0001 x A B R d dv_B_d dv_B_x = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0003 (A B R : SemanticCore.Class) : nb084AlphaDummy002 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_compact_envfresh_0002 (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_B_d : d ∉ B.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) : Nominal.TEnvFresh [(nb084AlphaDummy002 A B R, y), (nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)] B.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0002 (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_B_d : d ∉ B.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) : Nominal.TReflOn [(nb084AlphaDummy002 A B R, y), (nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)] B.fv

Checked nominal proof certificate identified upstream as nb084_focused_refl_0002.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0002 x y A B R d dv_B_d dv_B_x dv_B_y = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0004 (A B R : SemanticCore.Class) : nb084AlphaDummy003 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0005 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy005 x y A R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0006 (A B R : SemanticCore.Class) : nb084AlphaDummy002 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0007 (A B R : SemanticCore.Class) : nb084AlphaDummy001 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_compact_envfresh_0003 (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) : Nominal.TEnvFresh [(nb084AlphaDummy003 A B R, nb084AlphaDummy005 x y A R), (nb084AlphaDummy002 A B R, y), (nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)] A.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0003 (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) : Nominal.TReflOn [(nb084AlphaDummy003 A B R, nb084AlphaDummy005 x y A R), (nb084AlphaDummy002 A B R, y), (nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)] A.fv

Checked nominal proof certificate identified upstream as nb084_focused_refl_0003.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0003 x y A B R d dv_A_d dv_A_x dv_A_y = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0008 (A B R : SemanticCore.Class) : nb084AlphaDummy004 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_focused_notmem_0009 (x y : SemanticCore.Var) (A R : SemanticCore.Class) : nb084AlphaDummy006 x y A R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084_compact_envfresh_0004 (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) : Nominal.TEnvFresh [(nb084AlphaDummy004 A B R, nb084AlphaDummy006 x y A R), (nb084AlphaDummy003 A B R, nb084AlphaDummy005 x y A R), (nb084AlphaDummy002 A B R, y), (nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)] A.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0004 (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_d : d ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) : Nominal.TReflOn [(nb084AlphaDummy004 A B R, nb084AlphaDummy006 x y A R), (nb084AlphaDummy003 A B R, nb084AlphaDummy005 x y A R), (nb084AlphaDummy002 A B R, y), (nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)] A.fv

Checked nominal proof certificate identified upstream as nb084_focused_refl_0004.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0004 x y A B R d dv_A_d dv_A_x dv_A_y = ⋯.reflOn