LeanPool.NFWeakPartition.NAR4C083C001Part001

NF weak partition development: NAR4C083C001Part001.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy000 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_000.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy000 A B C R = NFChoice.ReplaySupport.freshVar (R.fv ∪ A.fv ∪ B.fv ∪ C.fv)

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy001 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_001.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy001 A B C R = NFChoice.ReplaySupport.freshVar (R.fv ∪ A.fv ∪ B.fv ∪ C.fv) 1

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy002 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_002.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy003 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_003.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy004 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_004.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy004 b c = NFChoice.ReplaySupport.freshVar ((NFChoice.SemanticCore.Class.cv b).fv ∪ (NFChoice.SemanticCore.Class.cv c).fv)

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy005 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_005.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy005 b c = NFChoice.ReplaySupport.freshVar ((NFChoice.SemanticCore.Class.cv b).fv ∪ (NFChoice.SemanticCore.Class.cv c).fv) 1

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy006 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_006.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy007 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_007.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy008 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_008.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy009 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_009.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy010 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_010.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy011 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_011.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy012 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_012.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy013 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_013.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy014 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_014.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy015 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_015.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy016 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_016.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy017 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_017.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy018 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_018.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy019 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_019.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy020 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_020.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy021 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_021.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy022 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_022.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy023 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_023.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy024 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_024.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy025 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_025.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy026 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_026.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy027 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_027.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy028 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_028.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy029 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_029.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy030 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_030.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy031 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_031.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy032 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_032.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy033 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_033.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy034 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_034.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy035 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_035.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy036 (A B C R : SemanticCore.Class) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_036.

Equations

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

Instances For

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083AlphaDummy037 (b c : SemanticCore.Var) :

SemanticCore.Var

Checked nominal proof certificate identified upstream as nb083_alpha_dummy_037.

Equations

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

Instances For

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_000 (A B C R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_001 (A B C R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_003 (b c : SemanticCore.Var) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_004 (A B C R : SemanticCore.Class) :

nb083AlphaDummy002 A B C R ∉ (SemanticCore.Class.cv (nb083AlphaDummy000 A B C R)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy001 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_005 (A B C R : SemanticCore.Class) :

nb083AlphaDummy003 A B C R ∉ (SemanticCore.Class.cv (nb083AlphaDummy000 A B C R)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy001 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_distinct_006 (A B C R : SemanticCore.Class) :

nb083AlphaDummy002 A B C R ≠ nb083AlphaDummy003 A B C R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_007 (A B C R : SemanticCore.Class) :

nb083AlphaDummy010 A B C R ∉ (SemanticCore.Class.cv (nb083AlphaDummy003 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_008 (A B C R : SemanticCore.Class) :

nb083AlphaDummy011 A B C R ∉ (SemanticCore.Class.cv (nb083AlphaDummy003 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_distinct_009 (A B C R : SemanticCore.Class) :

nb083AlphaDummy010 A B C R ≠ nb083AlphaDummy011 A B C R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_010 (b c : SemanticCore.Var) :

nb083AlphaDummy012 b c ∉ (SemanticCore.Class.cv (nb083AlphaDummy005 b c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_011 (b c : SemanticCore.Var) :

nb083AlphaDummy013 b c ∉ (SemanticCore.Class.cv (nb083AlphaDummy005 b c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_distinct_012 (b c : SemanticCore.Var) :

nb083AlphaDummy012 b c ≠ nb083AlphaDummy013 b c

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_013 (A B C R : SemanticCore.Class) :

nb083AlphaDummy016 A B C R ∉ (SemanticCore.Class.cv (nb083AlphaDummy010 A B C R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_014 (A B C R : SemanticCore.Class) :

nb083AlphaDummy017 A B C R ∉ (SemanticCore.Class.cv (nb083AlphaDummy010 A B C R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_015 (A B C R : SemanticCore.Class) :

nb083AlphaDummy018 A B C R ∉ (SemanticCore.Class.cv (nb083AlphaDummy010 A B C R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_distinct_016 (A B C R : SemanticCore.Class) :

nb083AlphaDummy016 A B C R ≠ nb083AlphaDummy017 A B C R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_distinct_017 (A B C R : SemanticCore.Class) :

nb083AlphaDummy016 A B C R ≠ nb083AlphaDummy018 A B C R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_distinct_018 (A B C R : SemanticCore.Class) :

nb083AlphaDummy017 A B C R ≠ nb083AlphaDummy018 A B C R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_019 (b c : SemanticCore.Var) :

nb083AlphaDummy019 b c ∉ (SemanticCore.Class.cv (nb083AlphaDummy012 b c)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_020 (b c : SemanticCore.Var) :

nb083AlphaDummy020 b c ∉ (SemanticCore.Class.cv (nb083AlphaDummy012 b c)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_021 (b c : SemanticCore.Var) :

nb083AlphaDummy021 b c ∉ (SemanticCore.Class.cv (nb083AlphaDummy012 b c)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_distinct_022 (b c : SemanticCore.Var) :

nb083AlphaDummy019 b c ≠ nb083AlphaDummy020 b c

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_distinct_023 (b c : SemanticCore.Var) :

nb083AlphaDummy019 b c ≠ nb083AlphaDummy021 b c

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_distinct_024 (b c : SemanticCore.Var) :

nb083AlphaDummy020 b c ≠ nb083AlphaDummy021 b c

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_025 (A B C R : SemanticCore.Class) :

nb083AlphaDummy028 A B C R ∉ (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_026 (A B C R : SemanticCore.Class) :

nb083AlphaDummy024 A B C R ∉ (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_027 (A B C R : SemanticCore.Class) :

nb083AlphaDummy030 A B C R ∉ (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_028 (b c : SemanticCore.Var) :

nb083AlphaDummy029 b c ∉ (SemanticCore.Class.cv (nb083AlphaDummy020 b c)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy020 b c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_029 (b c : SemanticCore.Var) :

nb083AlphaDummy025 b c ∉ (SemanticCore.Class.cv (nb083AlphaDummy020 b c)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy021 b c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_030 (b c : SemanticCore.Var) :

nb083AlphaDummy031 b c ∉ (SemanticCore.Class.cv (nb083AlphaDummy021 b c)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy021 b c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_031 (b c : SemanticCore.Var) :

nb083AlphaDummy004 b c ∉ (SemanticCore.Class.cv b).fv ∪ (SemanticCore.Class.cv c).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_032 (b c : SemanticCore.Var) :

nb083AlphaDummy005 b c ∉ (SemanticCore.Class.cv b).fv ∪ (SemanticCore.Class.cv c).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_distinct_033 (b c : SemanticCore.Var) :

nb083AlphaDummy004 b c ≠ nb083AlphaDummy005 b c

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_034 (A B C R : SemanticCore.Class) :

nb083AlphaDummy014 A B C R ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb083AlphaDummy010 A B C R)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb083AlphaDummy010 A B C R)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy010 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_035 (b c : SemanticCore.Var) :

nb083AlphaDummy015 b c ∉ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb083AlphaDummy012 b c)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb083AlphaDummy012 b c)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy012 b c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_036 (A B C R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_037 (b c : SemanticCore.Var) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_038 (A B C R : SemanticCore.Class) :

nb083AlphaDummy026 A B C R ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_039 (b c : SemanticCore.Var) :

nb083AlphaDummy027 b c ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy020 b c))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy021 b c))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_040 (A B C R : SemanticCore.Class) :

nb083AlphaDummy034 A B C R ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy003 A B C R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_041 (b c : SemanticCore.Var) :

nb083AlphaDummy035 b c ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy005 b c)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_042 (A B C R : SemanticCore.Class) :

nb083AlphaDummy022 A B C R ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)) (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)) (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_043 (b c : SemanticCore.Var) :

nb083AlphaDummy023 b c ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy020 b c)) (SemanticCore.Class.cv (nb083AlphaDummy021 b c))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy020 b c)) (SemanticCore.Class.cv (nb083AlphaDummy021 b c))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_044 (A B C R : SemanticCore.Class) :

nb083AlphaDummy036 A B C R ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy003 A B C R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy003 A B C R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_045 (b c : SemanticCore.Var) :

nb083AlphaDummy037 b c ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy005 b c))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy005 b c))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_046 (A B C R : SemanticCore.Class) :

nb083AlphaDummy000 A B C R ∉ R.fv ∪ A.fv ∪ B.fv ∪ C.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_fresh_047 (A B C R : SemanticCore.Class) :

nb083AlphaDummy001 A B C R ∉ R.fv ∪ A.fv ∪ B.fv ∪ C.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_distinct_048 (A B C R : SemanticCore.Class) :

nb083AlphaDummy000 A B C R ≠ nb083AlphaDummy001 A B C R

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0000 (A B C R : SemanticCore.Class) :

nb083AlphaDummy000 A B C R ∈ (SemanticCore.Class.cv (nb083AlphaDummy000 A B C R)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy001 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0001 (A B C R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0002 (b c : SemanticCore.Var) :

b ∈ (SemanticCore.Class.cv b).fv ∪ (SemanticCore.Class.cv c).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0003 (b c : SemanticCore.Var) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0004 (A B C R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0006 (A B C R : SemanticCore.Class) :

nb083AlphaDummy003 A B C R ∈ (SemanticCore.Class.cv (nb083AlphaDummy003 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0007 (b c : SemanticCore.Var) :

nb083AlphaDummy005 b c ∈ (SemanticCore.Class.cv (nb083AlphaDummy005 b c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0010 (A B C R : SemanticCore.Class) :

nb083AlphaDummy010 A B C R ∈ (SemanticCore.Class.cv (nb083AlphaDummy010 A B C R)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0011 (b c : SemanticCore.Var) :

nb083AlphaDummy012 b c ∈ (SemanticCore.Class.cv (nb083AlphaDummy012 b c)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0012 (A B C R : SemanticCore.Class) :

nb083AlphaDummy017 A B C R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)) (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)) (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0013 (b c : SemanticCore.Var) :

nb083AlphaDummy020 b c ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy020 b c)) (SemanticCore.Class.cv (nb083AlphaDummy021 b c))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy020 b c)) (SemanticCore.Class.cv (nb083AlphaDummy021 b c))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0014 (A B C R : SemanticCore.Class) :

nb083AlphaDummy017 A B C R ∈ (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0015 (b c : SemanticCore.Var) :

nb083AlphaDummy020 b c ∈ (SemanticCore.Class.cv (nb083AlphaDummy020 b c)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy021 b c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0016 (A B C R : SemanticCore.Class) :

nb083AlphaDummy018 A B C R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)) (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)) (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0017 (b c : SemanticCore.Var) :

nb083AlphaDummy021 b c ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy020 b c)) (SemanticCore.Class.cv (nb083AlphaDummy021 b c))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb083AlphaDummy020 b c)) (SemanticCore.Class.cv (nb083AlphaDummy021 b c))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0018 (A B C R : SemanticCore.Class) :

nb083AlphaDummy018 A B C R ∈ (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0019 (b c : SemanticCore.Var) :

nb083AlphaDummy021 b c ∈ (SemanticCore.Class.cv (nb083AlphaDummy020 b c)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy021 b c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0020 (A B C R : SemanticCore.Class) :

nb083AlphaDummy017 A B C R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0021 (b c : SemanticCore.Var) :

nb083AlphaDummy020 b c ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy020 b c))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy021 b c))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0022 (A B C R : SemanticCore.Class) :

nb083AlphaDummy017 A B C R ∈ (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0023 (b c : SemanticCore.Var) :

nb083AlphaDummy020 b c ∈ (SemanticCore.Class.cv (nb083AlphaDummy020 b c)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy020 b c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0024 (A B C R : SemanticCore.Class) :

nb083AlphaDummy018 A B C R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy017 A B C R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0025 (b c : SemanticCore.Var) :

nb083AlphaDummy021 b c ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy020 b c))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb083AlphaDummy021 b c))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0026 (A B C R : SemanticCore.Class) :

nb083AlphaDummy018 A B C R ∈ (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy018 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0027 (b c : SemanticCore.Var) :

nb083AlphaDummy021 b c ∈ (SemanticCore.Class.cv (nb083AlphaDummy021 b c)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy021 b c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0028 (A B C R : SemanticCore.Class) :

nb083AlphaDummy001 A B C R ∈ (SemanticCore.Class.cv (nb083AlphaDummy000 A B C R)).fv ∪ (SemanticCore.Class.cv (nb083AlphaDummy001 A B C R)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0029 (A B C R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0030 (b c : SemanticCore.Var) :

c ∈ (SemanticCore.Class.cv b).fv ∪ (SemanticCore.Class.cv c).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0031 (b c : SemanticCore.Var) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0032 (A B C R : SemanticCore.Class) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0033 (b c : SemanticCore.Var) :

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0034 (A B C R : SemanticCore.Class) :

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

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0035 (b c : SemanticCore.Var) :

nb083AlphaDummy005 b c ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy005 b c)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0036 (A B C R : SemanticCore.Class) :

nb083AlphaDummy003 A B C R ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy003 A B C R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy003 A B C R))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_support_mem_0037 (b c : SemanticCore.Var) :

nb083AlphaDummy005 b c ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy005 b c))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb083AlphaDummy005 b c))).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_focused_notmem_0000 (A B C R : SemanticCore.Class) :

nb083AlphaDummy000 A B C R ∉ A.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_compact_envfresh_0000 (A B C R : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) :

Nominal.TEnvFresh [(nb083AlphaDummy000 A B C R, b)] A.fv

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083FocusedRefl0000 (A B C R : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) :

Nominal.TReflOn [(nb083AlphaDummy000 A B C R, b)] A.fv

Checked nominal proof certificate identified upstream as nb083_focused_refl_0000.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083FocusedRefl0000 A B C R b dv_A_b = ⋯.reflOn

Instances For

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_focused_notmem_0001 (A B C R : SemanticCore.Class) :

nb083AlphaDummy000 A B C R ∉ B.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_focused_notmem_0002 (A B C R : SemanticCore.Class) :

nb083AlphaDummy000 A B C R ∉ C.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_wpp_notmem_0000 (A B C R : SemanticCore.Class) :

nb083AlphaDummy000 A B C R ∉ (Compiler.CompactSourceSyntax.synCsep2 B C).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_wpp_notmem_0001 (B C : SemanticCore.Class) (b : SemanticCore.Var) (dv_B_b : b ∉ B.fv) (dv_C_b : b ∉ C.fv) :

b ∉ (Compiler.CompactSourceSyntax.synCsep2 B C).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_compact_envfresh_0001 (A B C R : SemanticCore.Class) (b : SemanticCore.Var) (dv_B_b : b ∉ B.fv) (dv_C_b : b ∉ C.fv) :

Nominal.TEnvFresh [(nb083AlphaDummy000 A B C R, b)] (Compiler.CompactSourceSyntax.synCsep2 B C).fv

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083WppRefl0000 (A B C R : SemanticCore.Class) (b : SemanticCore.Var) (dv_B_b : b ∉ B.fv) (dv_C_b : b ∉ C.fv) :

Nominal.TReflOn [(nb083AlphaDummy000 A B C R, b)] (Compiler.CompactSourceSyntax.synCsep2 B C).fv

Checked nominal proof certificate identified upstream as nb083_wpp_refl_0000.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083WppRefl0000 A B C R b dv_B_b dv_C_b = ⋯.reflOn

Instances For

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_focused_notmem_0003 (A B C R : SemanticCore.Class) :

nb083AlphaDummy001 A B C R ∉ A.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_compact_envfresh_0002 (A B C R : SemanticCore.Class) (b c : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_c : c ∉ A.fv) :

Nominal.TEnvFresh [(nb083AlphaDummy001 A B C R, c), (nb083AlphaDummy000 A B C R, b)] A.fv

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083FocusedRefl0001 (A B C R : SemanticCore.Class) (b c : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_c : c ∉ A.fv) :

Nominal.TReflOn [(nb083AlphaDummy001 A B C R, c), (nb083AlphaDummy000 A B C R, b)] A.fv

Checked nominal proof certificate identified upstream as nb083_focused_refl_0001.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083FocusedRefl0001 A B C R b c dv_A_b dv_A_c = ⋯.reflOn

Instances For

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_focused_notmem_0004 (A B C R : SemanticCore.Class) :

nb083AlphaDummy001 A B C R ∉ B.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_focused_notmem_0005 (A B C R : SemanticCore.Class) :

nb083AlphaDummy001 A B C R ∉ C.fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_wpp_notmem_0002 (A B C R : SemanticCore.Class) :

nb083AlphaDummy001 A B C R ∉ (Compiler.CompactSourceSyntax.synCsep2 B C).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_wpp_notmem_0003 (B C : SemanticCore.Class) (c : SemanticCore.Var) (dv_B_c : c ∉ B.fv) (dv_C_c : c ∉ C.fv) :

c ∉ (Compiler.CompactSourceSyntax.synCsep2 B C).fv

source

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083_compact_envfresh_0003 (A B C R : SemanticCore.Class) (b c : SemanticCore.Var) (dv_B_b : b ∉ B.fv) (dv_B_c : c ∉ B.fv) (dv_C_b : b ∉ C.fv) (dv_C_c : c ∉ C.fv) :

Nominal.TEnvFresh [(nb083AlphaDummy001 A B C R, c), (nb083AlphaDummy000 A B C R, b)] (Compiler.CompactSourceSyntax.synCsep2 B C).fv

source

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083WppRefl0001 (A B C R : SemanticCore.Class) (b c : SemanticCore.Var) (dv_B_b : b ∉ B.fv) (dv_B_c : c ∉ B.fv) (dv_C_b : b ∉ C.fv) (dv_C_c : c ∉ C.fv) :

Nominal.TReflOn [(nb083AlphaDummy001 A B C R, c), (nb083AlphaDummy000 A B C R, b)] (Compiler.CompactSourceSyntax.synCsep2 B C).fv

Checked nominal proof certificate identified upstream as nb083_wpp_refl_0001.

Equations

NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083WppRefl0001 A B C R b c dv_B_b dv_B_c dv_C_b dv_C_c = ⋯.reflOn

Instances For