LeanPool.NFWeakPartition.NAR4C066C001Part001

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy000 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_000.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy000 A R = NFChoice.ReplaySupport.freshVar (A.fv ∪ R.fv)

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy001 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_001.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy001 A R = NFChoice.ReplaySupport.freshVar (A.fv ∪ R.fv) 1

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy002 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_002.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy003 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_003.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy004 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_004.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy005 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_005.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy006 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_006.

Equations

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

Instances For

source

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

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_007.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy007 x = NFChoice.ReplaySupport.freshVar (NFChoice.SemanticCore.Class.cv x).fv

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy008 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_008.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy009 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_009.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy010 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_010.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy011 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_011.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy012 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_012.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy013 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_013.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy014 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_014.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy015 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_015.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy016 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_016.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy017 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_017.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy018 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_018.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy019 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_019.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy020 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_020.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy021 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_021.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy022 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_022.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy023 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_023.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy024 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_024.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy025 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_025.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy026 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_026.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy027 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_027.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy028 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_028.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy029 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_029.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy030 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_030.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy031 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_031.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy032 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_032.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy033 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_033.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy034 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_034.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy035 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_035.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy036 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_036.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy037 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_037.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy038 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_038.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy039 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_039.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy040 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_040.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy041 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_041.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy042 (A R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_042.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066AlphaDummy043 (x : SemanticCore.Var) (R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb066_alpha_dummy_043.

Equations

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

Instances For

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_000 (A R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_001 (A R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_002 (x : SemanticCore.Var) (R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_003 (x : SemanticCore.Var) (R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_004 (A R : SemanticCore.Class) :

nb066AlphaDummy006 A R ∉ (SemanticCore.Class.cv (nb066AlphaDummy000 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_005 (A R : SemanticCore.Class) :

nb066AlphaDummy008 A R ∉ (SemanticCore.Class.cv (nb066AlphaDummy003 A R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy002 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_006 (A R : SemanticCore.Class) :

nb066AlphaDummy009 A R ∉ (SemanticCore.Class.cv (nb066AlphaDummy003 A R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy002 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_007 (A R : SemanticCore.Class) :

nb066AlphaDummy008 A R ≠ nb066AlphaDummy009 A R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_008 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy010 x R ∉ (SemanticCore.Class.cv (nb066AlphaDummy005 x R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy004 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_009 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy011 x R ∉ (SemanticCore.Class.cv (nb066AlphaDummy005 x R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy004 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_010 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy010 x R ≠ nb066AlphaDummy011 x R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_011 (A R : SemanticCore.Class) :

nb066AlphaDummy016 A R ∉ (SemanticCore.Class.cv (nb066AlphaDummy009 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_012 (A R : SemanticCore.Class) :

nb066AlphaDummy017 A R ∉ (SemanticCore.Class.cv (nb066AlphaDummy009 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_013 (A R : SemanticCore.Class) :

nb066AlphaDummy016 A R ≠ nb066AlphaDummy017 A R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_014 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy018 x R ∉ (SemanticCore.Class.cv (nb066AlphaDummy011 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_015 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy019 x R ∉ (SemanticCore.Class.cv (nb066AlphaDummy011 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_016 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy018 x R ≠ nb066AlphaDummy019 x R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_017 (A R : SemanticCore.Class) :

nb066AlphaDummy022 A R ∉ (SemanticCore.Class.cv (nb066AlphaDummy016 A R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_018 (A R : SemanticCore.Class) :

nb066AlphaDummy023 A R ∉ (SemanticCore.Class.cv (nb066AlphaDummy016 A R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_019 (A R : SemanticCore.Class) :

nb066AlphaDummy024 A R ∉ (SemanticCore.Class.cv (nb066AlphaDummy016 A R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_020 (A R : SemanticCore.Class) :

nb066AlphaDummy022 A R ≠ nb066AlphaDummy023 A R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_021 (A R : SemanticCore.Class) :

nb066AlphaDummy022 A R ≠ nb066AlphaDummy024 A R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_022 (A R : SemanticCore.Class) :

nb066AlphaDummy023 A R ≠ nb066AlphaDummy024 A R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_023 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy025 x R ∉ (SemanticCore.Class.cv (nb066AlphaDummy018 x R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_024 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy026 x R ∉ (SemanticCore.Class.cv (nb066AlphaDummy018 x R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_025 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy027 x R ∉ (SemanticCore.Class.cv (nb066AlphaDummy018 x R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_026 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy025 x R ≠ nb066AlphaDummy026 x R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_027 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy025 x R ≠ nb066AlphaDummy027 x R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_028 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy026 x R ≠ nb066AlphaDummy027 x R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_029 (A R : SemanticCore.Class) :

nb066AlphaDummy034 A R ∉ (SemanticCore.Class.cv (nb066AlphaDummy023 A R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy023 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_030 (A R : SemanticCore.Class) :

nb066AlphaDummy030 A R ∉ (SemanticCore.Class.cv (nb066AlphaDummy023 A R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy024 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_031 (A R : SemanticCore.Class) :

nb066AlphaDummy036 A R ∉ (SemanticCore.Class.cv (nb066AlphaDummy024 A R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy024 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_032 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy035 x R ∉ (SemanticCore.Class.cv (nb066AlphaDummy026 x R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy026 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_033 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy031 x R ∉ (SemanticCore.Class.cv (nb066AlphaDummy026 x R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy027 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_034 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy037 x R ∉ (SemanticCore.Class.cv (nb066AlphaDummy027 x R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy027 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_035 (x : SemanticCore.Var) :

nb066AlphaDummy007 x ∉ (SemanticCore.Class.cv x).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_036 (A R : SemanticCore.Class) :

nb066AlphaDummy020 A R ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb066AlphaDummy016 A R)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb066AlphaDummy016 A R)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy016 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_038 (A R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_039 (x : SemanticCore.Var) (R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_040 (A R : SemanticCore.Class) :

nb066AlphaDummy032 A R ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy023 A R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy024 A R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_041 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy033 x R ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy026 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy027 x R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_042 (A R : SemanticCore.Class) :

nb066AlphaDummy040 A R ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy009 A R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_043 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy041 x R ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy011 x R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_044 (A R : SemanticCore.Class) :

nb066AlphaDummy028 A R ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy023 A R)) (SemanticCore.Class.cv (nb066AlphaDummy024 A R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy023 A R)) (SemanticCore.Class.cv (nb066AlphaDummy024 A R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_045 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy029 x R ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy026 x R)) (SemanticCore.Class.cv (nb066AlphaDummy027 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy026 x R)) (SemanticCore.Class.cv (nb066AlphaDummy027 x R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_046 (A R : SemanticCore.Class) :

nb066AlphaDummy042 A R ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy009 A R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy009 A R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_047 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy043 x R ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy011 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy011 x R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_048 (A R : SemanticCore.Class) :

nb066AlphaDummy000 A R ∉ A.fv ∪ R.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_049 (A R : SemanticCore.Class) :

nb066AlphaDummy001 A R ∉ A.fv ∪ R.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_050 (A R : SemanticCore.Class) :

nb066AlphaDummy000 A R ≠ nb066AlphaDummy001 A R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_051 (A R : SemanticCore.Class) :

nb066AlphaDummy002 A R ∉ R.fv ∪ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb066AlphaDummy000 A R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_052 (A R : SemanticCore.Class) :

nb066AlphaDummy003 A R ∉ R.fv ∪ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb066AlphaDummy000 A R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_053 (A R : SemanticCore.Class) :

nb066AlphaDummy002 A R ≠ nb066AlphaDummy003 A R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_054 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy004 x R ∉ R.fv ∪ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_fresh_055 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy005 x R ∉ R.fv ∪ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_distinct_056 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy004 x R ≠ nb066AlphaDummy005 x R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0000 (A R : SemanticCore.Class) :

nb066AlphaDummy000 A R ∈ R.fv ∪ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb066AlphaDummy000 A R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0001 (x : SemanticCore.Var) (R : SemanticCore.Class) :

x ∈ R.fv ∪ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0002 (A R : SemanticCore.Class) :

nb066AlphaDummy000 A R ∈ (SemanticCore.Class.cv (nb066AlphaDummy000 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0003 (x : SemanticCore.Var) :

x ∈ (SemanticCore.Class.cv x).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0004 (A R : SemanticCore.Class) :

nb066AlphaDummy003 A R ∈ (SemanticCore.Class.cv (nb066AlphaDummy003 A R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy002 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0005 (A R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0006 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy005 x R ∈ (SemanticCore.Class.cv (nb066AlphaDummy005 x R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy004 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0007 (x : SemanticCore.Var) (R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0008 (A R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0009 (x : SemanticCore.Var) (R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0010 (A R : SemanticCore.Class) :

nb066AlphaDummy009 A R ∈ (SemanticCore.Class.cv (nb066AlphaDummy009 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0011 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy011 x R ∈ (SemanticCore.Class.cv (nb066AlphaDummy011 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0014 (A R : SemanticCore.Class) :

nb066AlphaDummy016 A R ∈ (SemanticCore.Class.cv (nb066AlphaDummy016 A R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0015 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy018 x R ∈ (SemanticCore.Class.cv (nb066AlphaDummy018 x R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0016 (A R : SemanticCore.Class) :

nb066AlphaDummy023 A R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy023 A R)) (SemanticCore.Class.cv (nb066AlphaDummy024 A R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy023 A R)) (SemanticCore.Class.cv (nb066AlphaDummy024 A R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0017 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy026 x R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy026 x R)) (SemanticCore.Class.cv (nb066AlphaDummy027 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy026 x R)) (SemanticCore.Class.cv (nb066AlphaDummy027 x R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0018 (A R : SemanticCore.Class) :

nb066AlphaDummy023 A R ∈ (SemanticCore.Class.cv (nb066AlphaDummy023 A R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy024 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0019 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy026 x R ∈ (SemanticCore.Class.cv (nb066AlphaDummy026 x R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy027 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0020 (A R : SemanticCore.Class) :

nb066AlphaDummy024 A R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy023 A R)) (SemanticCore.Class.cv (nb066AlphaDummy024 A R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy023 A R)) (SemanticCore.Class.cv (nb066AlphaDummy024 A R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0021 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy027 x R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy026 x R)) (SemanticCore.Class.cv (nb066AlphaDummy027 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb066AlphaDummy026 x R)) (SemanticCore.Class.cv (nb066AlphaDummy027 x R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0022 (A R : SemanticCore.Class) :

nb066AlphaDummy024 A R ∈ (SemanticCore.Class.cv (nb066AlphaDummy023 A R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy024 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0023 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy027 x R ∈ (SemanticCore.Class.cv (nb066AlphaDummy026 x R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy027 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0024 (A R : SemanticCore.Class) :

nb066AlphaDummy023 A R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy023 A R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy024 A R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0025 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy026 x R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy026 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy027 x R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0026 (A R : SemanticCore.Class) :

nb066AlphaDummy023 A R ∈ (SemanticCore.Class.cv (nb066AlphaDummy023 A R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy023 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0027 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy026 x R ∈ (SemanticCore.Class.cv (nb066AlphaDummy026 x R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy026 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0028 (A R : SemanticCore.Class) :

nb066AlphaDummy024 A R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy023 A R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy024 A R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0029 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy027 x R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy026 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb066AlphaDummy027 x R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0030 (A R : SemanticCore.Class) :

nb066AlphaDummy024 A R ∈ (SemanticCore.Class.cv (nb066AlphaDummy024 A R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy024 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0031 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy027 x R ∈ (SemanticCore.Class.cv (nb066AlphaDummy027 x R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy027 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0032 (A R : SemanticCore.Class) :

nb066AlphaDummy002 A R ∈ (SemanticCore.Class.cv (nb066AlphaDummy003 A R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy002 A R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0033 (A R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0034 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy004 x R ∈ (SemanticCore.Class.cv (nb066AlphaDummy005 x R)).fv ∪ (SemanticCore.Class.cv (nb066AlphaDummy004 x R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0035 (x : SemanticCore.Var) (R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0036 (A R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0037 (x : SemanticCore.Var) (R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0038 (A R : SemanticCore.Class) :

nb066AlphaDummy009 A R ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy009 A R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0039 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy011 x R ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy011 x R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0040 (A R : SemanticCore.Class) :

nb066AlphaDummy009 A R ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy009 A R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy009 A R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_support_mem_0041 (x : SemanticCore.Var) (R : SemanticCore.Class) :

nb066AlphaDummy011 x R ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy011 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb066AlphaDummy011 x R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_focused_notmem_0000 (A R : SemanticCore.Class) :

nb066AlphaDummy000 A R ∉ A.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0000 (A R : SemanticCore.Class) :

nb066AlphaDummy000 A R ∉ A.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0001 (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) :

x ∉ A.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_focused_notmem_0001 (A R : SemanticCore.Class) :

nb066AlphaDummy001 A R ∉ A.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0002 (A R : SemanticCore.Class) :

nb066AlphaDummy001 A R ∉ A.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_wpp_notmem_0003 (y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_y : y ∉ A.fv) :

y ∉ A.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb066_compact_envfresh_0000 (x y : SemanticCore.Var) (A R : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) :

Nominal.TEnvFresh [(nb066AlphaDummy000 A R, x), (nb066AlphaDummy001 A R, y)] A.fv