Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C078C001Block005

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C078C001Part022.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0033 :

nb078AlphaDummy010 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy017 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy018 (SemanticCore.Class.cv nb078AlphaDummy009) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy017) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy017 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy018 (SemanticCore.Class.cv nb078AlphaDummy010) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy017) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0034 (f : SemanticCore.Var) :

nb078AlphaDummy013 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy012 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy013 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0035 (f : SemanticCore.Var) :

nb078AlphaDummy013 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy019 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy020 f) (SemanticCore.Class.cv (nb078AlphaDummy012 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy019 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy019 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy020 f) (SemanticCore.Class.cv (nb078AlphaDummy013 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy019 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0036 :

nb078AlphaDummy010 ∈ (SemanticCore.Class.cab nb078AlphaDummy017 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy018 (SemanticCore.Class.cv nb078AlphaDummy010) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy017) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy017 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy018 (SemanticCore.Class.cv nb078AlphaDummy010) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy017) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0037 (f : SemanticCore.Var) :

nb078AlphaDummy013 f ∈ (SemanticCore.Class.cab (nb078AlphaDummy019 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy020 f) (SemanticCore.Class.cv (nb078AlphaDummy013 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy019 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy019 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy020 f) (SemanticCore.Class.cv (nb078AlphaDummy013 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy019 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0038 :

nb078AlphaDummy018 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0039 (f : SemanticCore.Var) :

nb078AlphaDummy020 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0040 :

nb078AlphaDummy018 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy018)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0041 (f : SemanticCore.Var) :

nb078AlphaDummy020 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy020 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0042 :

nb078AlphaDummy009 ∈ (SemanticCore.Class.cv nb078AlphaDummy009).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy011).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0043 :

nb078AlphaDummy009 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy054 (SemanticCore.Class.cv nb078AlphaDummy009) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy053) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy054 (SemanticCore.Class.cv nb078AlphaDummy011) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0044 (f : SemanticCore.Var) :

nb078AlphaDummy012 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy012 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy014 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0045 (f : SemanticCore.Var) :

nb078AlphaDummy012 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy056 f) (SemanticCore.Class.cv (nb078AlphaDummy012 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy056 f) (SemanticCore.Class.cv (nb078AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0047 (f : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0048 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0049 (f : SemanticCore.Var) :

nb078AlphaDummy056 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy056 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0050 :

nb078AlphaDummy061 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy061) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy061) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy061).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0052 :

nb078AlphaDummy061 ∈ (SemanticCore.Class.cv nb078AlphaDummy061).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0053 (f : SemanticCore.Var) :

nb078AlphaDummy063 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy063 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0054 :

nb078AlphaDummy068 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy068) (SemanticCore.Class.cv nb078AlphaDummy069)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy068) (SemanticCore.Class.cv nb078AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0055 (f : SemanticCore.Var) :

nb078AlphaDummy071 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy071 f)) (SemanticCore.Class.cv (nb078AlphaDummy072 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy071 f)) (SemanticCore.Class.cv (nb078AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0056 :

nb078AlphaDummy068 ∈ (SemanticCore.Class.cv nb078AlphaDummy068).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy069).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0057 (f : SemanticCore.Var) :

nb078AlphaDummy071 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy071 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy072 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0058 :

nb078AlphaDummy069 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy068) (SemanticCore.Class.cv nb078AlphaDummy069)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy068) (SemanticCore.Class.cv nb078AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0059 (f : SemanticCore.Var) :

nb078AlphaDummy072 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy071 f)) (SemanticCore.Class.cv (nb078AlphaDummy072 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy071 f)) (SemanticCore.Class.cv (nb078AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0060 :

nb078AlphaDummy069 ∈ (SemanticCore.Class.cv nb078AlphaDummy068).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy069).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0061 (f : SemanticCore.Var) :

nb078AlphaDummy072 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy071 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy072 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0062 :

nb078AlphaDummy068 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy068)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0063 (f : SemanticCore.Var) :

nb078AlphaDummy071 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy071 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0064 :

nb078AlphaDummy068 ∈ (SemanticCore.Class.cv nb078AlphaDummy068).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy068).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0065 (f : SemanticCore.Var) :

nb078AlphaDummy071 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy071 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy071 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0066 :

nb078AlphaDummy069 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy068)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy069)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0067 (f : SemanticCore.Var) :

nb078AlphaDummy072 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy071 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy072 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0068 :

nb078AlphaDummy069 ∈ (SemanticCore.Class.cv nb078AlphaDummy069).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy069).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0069 (f : SemanticCore.Var) :

nb078AlphaDummy072 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy072 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy072 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0070 :

nb078AlphaDummy011 ∈ (SemanticCore.Class.cv nb078AlphaDummy009).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy011).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0071 :

nb078AlphaDummy011 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy054 (SemanticCore.Class.cv nb078AlphaDummy009) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy053) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy054 (SemanticCore.Class.cv nb078AlphaDummy011) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0072 (f : SemanticCore.Var) :

nb078AlphaDummy014 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy012 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy014 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0073 (f : SemanticCore.Var) :

nb078AlphaDummy014 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy056 f) (SemanticCore.Class.cv (nb078AlphaDummy012 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy056 f) (SemanticCore.Class.cv (nb078AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0074 :

nb078AlphaDummy011 ∈ (SemanticCore.Class.cab nb078AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy054 (SemanticCore.Class.cv nb078AlphaDummy011) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy054 (SemanticCore.Class.cv nb078AlphaDummy011) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0075 (f : SemanticCore.Var) :

nb078AlphaDummy014 f ∈ (SemanticCore.Class.cab (nb078AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy056 f) (SemanticCore.Class.cv (nb078AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy056 f) (SemanticCore.Class.cv (nb078AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0076 :

nb078AlphaDummy054 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0077 (f : SemanticCore.Var) :

nb078AlphaDummy056 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0078 :

nb078AlphaDummy054 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy054)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0079 (f : SemanticCore.Var) :

nb078AlphaDummy056 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy056 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0084 :

nb078AlphaDummy089 ∈ (SemanticCore.Class.cv nb078AlphaDummy089).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy090).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0085 :

nb078AlphaDummy089 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy095 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy096 (SemanticCore.Class.cv nb078AlphaDummy089) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy095) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy095 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy096 (SemanticCore.Class.cv nb078AlphaDummy090) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy095) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0086 (f : SemanticCore.Var) :

nb078AlphaDummy091 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy091 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy092 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0087 (f : SemanticCore.Var) :

nb078AlphaDummy091 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy097 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy098 f) (SemanticCore.Class.cv (nb078AlphaDummy091 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy097 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy097 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy098 f) (SemanticCore.Class.cv (nb078AlphaDummy092 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy097 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0089 (f : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0090 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0091 (f : SemanticCore.Var) :

nb078AlphaDummy098 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy098 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0092 :

nb078AlphaDummy103 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy103) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy103) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy103).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0094 :

nb078AlphaDummy103 ∈ (SemanticCore.Class.cv nb078AlphaDummy103).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0095 (f : SemanticCore.Var) :

nb078AlphaDummy105 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy105 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0096 :

nb078AlphaDummy110 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy110) (SemanticCore.Class.cv nb078AlphaDummy111)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy110) (SemanticCore.Class.cv nb078AlphaDummy111)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0097 (f : SemanticCore.Var) :

nb078AlphaDummy113 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy113 f)) (SemanticCore.Class.cv (nb078AlphaDummy114 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy113 f)) (SemanticCore.Class.cv (nb078AlphaDummy114 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0098 :

nb078AlphaDummy110 ∈ (SemanticCore.Class.cv nb078AlphaDummy110).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy111).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0099 (f : SemanticCore.Var) :

nb078AlphaDummy113 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy113 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy114 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0100 :

nb078AlphaDummy111 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy110) (SemanticCore.Class.cv nb078AlphaDummy111)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy110) (SemanticCore.Class.cv nb078AlphaDummy111)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0101 (f : SemanticCore.Var) :

nb078AlphaDummy114 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy113 f)) (SemanticCore.Class.cv (nb078AlphaDummy114 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy113 f)) (SemanticCore.Class.cv (nb078AlphaDummy114 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0102 :

nb078AlphaDummy111 ∈ (SemanticCore.Class.cv nb078AlphaDummy110).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy111).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0103 (f : SemanticCore.Var) :

nb078AlphaDummy114 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy113 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy114 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0104 :

nb078AlphaDummy110 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy110)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy111)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0105 (f : SemanticCore.Var) :

nb078AlphaDummy113 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy113 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy114 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0106 :

nb078AlphaDummy110 ∈ (SemanticCore.Class.cv nb078AlphaDummy110).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy110).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0107 (f : SemanticCore.Var) :

nb078AlphaDummy113 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy113 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy113 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0108 :

nb078AlphaDummy111 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy110)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy111)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0109 (f : SemanticCore.Var) :

nb078AlphaDummy114 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy113 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy114 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0110 :

nb078AlphaDummy111 ∈ (SemanticCore.Class.cv nb078AlphaDummy111).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy111).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0111 (f : SemanticCore.Var) :

nb078AlphaDummy114 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy114 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy114 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0112 :

nb078AlphaDummy090 ∈ (SemanticCore.Class.cv nb078AlphaDummy089).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy090).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0113 :

nb078AlphaDummy090 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy095 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy096 (SemanticCore.Class.cv nb078AlphaDummy089) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy095) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy095 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy096 (SemanticCore.Class.cv nb078AlphaDummy090) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy095) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0114 (f : SemanticCore.Var) :

nb078AlphaDummy092 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy091 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy092 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0115 (f : SemanticCore.Var) :

nb078AlphaDummy092 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy097 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy098 f) (SemanticCore.Class.cv (nb078AlphaDummy091 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy097 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy097 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy098 f) (SemanticCore.Class.cv (nb078AlphaDummy092 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy097 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0116 :

nb078AlphaDummy090 ∈ (SemanticCore.Class.cab nb078AlphaDummy095 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy096 (SemanticCore.Class.cv nb078AlphaDummy090) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy095) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy095 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy096 (SemanticCore.Class.cv nb078AlphaDummy090) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy095) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0117 (f : SemanticCore.Var) :

nb078AlphaDummy092 f ∈ (SemanticCore.Class.cab (nb078AlphaDummy097 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy098 f) (SemanticCore.Class.cv (nb078AlphaDummy092 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy097 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy097 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy098 f) (SemanticCore.Class.cv (nb078AlphaDummy092 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy097 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0118 :

nb078AlphaDummy096 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0119 (f : SemanticCore.Var) :

nb078AlphaDummy098 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0120 :

nb078AlphaDummy096 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy096)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0121 (f : SemanticCore.Var) :

nb078AlphaDummy098 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy098 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0122 :

nb078AlphaDummy090 ∈ (SemanticCore.Class.cv nb078AlphaDummy090).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy089).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0123 :

nb078AlphaDummy090 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy132 (SemanticCore.Class.cv nb078AlphaDummy090) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy131) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy132 (SemanticCore.Class.cv nb078AlphaDummy089) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0124 (f : SemanticCore.Var) :

nb078AlphaDummy092 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy092 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy091 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0125 (f : SemanticCore.Var) :

nb078AlphaDummy092 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy134 f) (SemanticCore.Class.cv (nb078AlphaDummy092 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy134 f) (SemanticCore.Class.cv (nb078AlphaDummy091 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0127 (f : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0128 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0129 (f : SemanticCore.Var) :

nb078AlphaDummy134 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy134 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0130 :

nb078AlphaDummy139 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy139) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy139).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0132 :

nb078AlphaDummy139 ∈ (SemanticCore.Class.cv nb078AlphaDummy139).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0133 (f : SemanticCore.Var) :

nb078AlphaDummy141 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy141 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0134 :

nb078AlphaDummy146 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy146) (SemanticCore.Class.cv nb078AlphaDummy147)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy146) (SemanticCore.Class.cv nb078AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0135 (f : SemanticCore.Var) :

nb078AlphaDummy149 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy149 f)) (SemanticCore.Class.cv (nb078AlphaDummy150 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy149 f)) (SemanticCore.Class.cv (nb078AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0136 :

nb078AlphaDummy146 ∈ (SemanticCore.Class.cv nb078AlphaDummy146).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy147).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0137 (f : SemanticCore.Var) :

nb078AlphaDummy149 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy149 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy150 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0138 :

nb078AlphaDummy147 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy146) (SemanticCore.Class.cv nb078AlphaDummy147)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy146) (SemanticCore.Class.cv nb078AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0139 (f : SemanticCore.Var) :

nb078AlphaDummy150 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy149 f)) (SemanticCore.Class.cv (nb078AlphaDummy150 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy149 f)) (SemanticCore.Class.cv (nb078AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0140 :

nb078AlphaDummy147 ∈ (SemanticCore.Class.cv nb078AlphaDummy146).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy147).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0141 (f : SemanticCore.Var) :

nb078AlphaDummy150 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy149 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy150 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0142 :

nb078AlphaDummy146 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy146)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0143 (f : SemanticCore.Var) :

nb078AlphaDummy149 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy149 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0144 :

nb078AlphaDummy146 ∈ (SemanticCore.Class.cv nb078AlphaDummy146).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy146).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0145 (f : SemanticCore.Var) :

nb078AlphaDummy149 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy149 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy149 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0146 :

nb078AlphaDummy147 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy146)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy147)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0147 (f : SemanticCore.Var) :

nb078AlphaDummy150 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy149 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy150 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0148 :

nb078AlphaDummy147 ∈ (SemanticCore.Class.cv nb078AlphaDummy147).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy147).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0149 (f : SemanticCore.Var) :

nb078AlphaDummy150 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy150 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy150 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0150 :

nb078AlphaDummy089 ∈ (SemanticCore.Class.cv nb078AlphaDummy090).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy089).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0151 :

nb078AlphaDummy089 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy132 (SemanticCore.Class.cv nb078AlphaDummy090) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy131) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy132 (SemanticCore.Class.cv nb078AlphaDummy089) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0152 (f : SemanticCore.Var) :

nb078AlphaDummy091 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy092 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy091 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0153 (f : SemanticCore.Var) :

nb078AlphaDummy091 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy134 f) (SemanticCore.Class.cv (nb078AlphaDummy092 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy134 f) (SemanticCore.Class.cv (nb078AlphaDummy091 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0154 :

nb078AlphaDummy089 ∈ (SemanticCore.Class.cab nb078AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy132 (SemanticCore.Class.cv nb078AlphaDummy089) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy132 (SemanticCore.Class.cv nb078AlphaDummy089) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0155 (f : SemanticCore.Var) :

nb078AlphaDummy091 f ∈ (SemanticCore.Class.cab (nb078AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy134 f) (SemanticCore.Class.cv (nb078AlphaDummy091 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy134 f) (SemanticCore.Class.cv (nb078AlphaDummy091 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0156 :

nb078AlphaDummy132 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0157 (f : SemanticCore.Var) :

nb078AlphaDummy134 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0158 :

nb078AlphaDummy132 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy132)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0159 (f : SemanticCore.Var) :

nb078AlphaDummy134 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy134 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0161 (f : SemanticCore.Var) :

f ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0162 :

nb078AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb078AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy000))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0163 (f : SemanticCore.Var) :

f ∈ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0164 :

nb078AlphaDummy000 ∈ (SemanticCore.Class.cv nb078AlphaDummy000).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy000)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0166 (f : SemanticCore.Var) :

f ∈ (SemanticCore.Class.cv f).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0169 (f : SemanticCore.Var) :

f ∈ {nb078AlphaDummy091 f} ∪ {nb078AlphaDummy092 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy092 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb078AlphaDummy091 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0170 :

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

Certificates from NAR4C078C001Part023.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0171 (f : SemanticCore.Var) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0172 :

nb078AlphaDummy011 ∈ (SemanticCore.Class.cv nb078AlphaDummy011).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy010).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0173 :

nb078AlphaDummy011 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy168 (SemanticCore.Class.cv nb078AlphaDummy011) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy167) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy168 (SemanticCore.Class.cv nb078AlphaDummy010) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0174 (f : SemanticCore.Var) :

nb078AlphaDummy014 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy014 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy013 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0175 (f : SemanticCore.Var) :

nb078AlphaDummy014 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy170 f) (SemanticCore.Class.cv (nb078AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy170 f) (SemanticCore.Class.cv (nb078AlphaDummy013 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0177 (f : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0178 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0179 (f : SemanticCore.Var) :

nb078AlphaDummy170 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy170 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0180 :

nb078AlphaDummy175 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy175) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy175).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0182 :

nb078AlphaDummy175 ∈ (SemanticCore.Class.cv nb078AlphaDummy175).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0183 (f : SemanticCore.Var) :

nb078AlphaDummy177 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy177 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0184 :

nb078AlphaDummy182 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy182) (SemanticCore.Class.cv nb078AlphaDummy183)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy182) (SemanticCore.Class.cv nb078AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0185 (f : SemanticCore.Var) :

nb078AlphaDummy185 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy185 f)) (SemanticCore.Class.cv (nb078AlphaDummy186 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy185 f)) (SemanticCore.Class.cv (nb078AlphaDummy186 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0186 :

nb078AlphaDummy182 ∈ (SemanticCore.Class.cv nb078AlphaDummy182).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy183).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0187 (f : SemanticCore.Var) :

nb078AlphaDummy185 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy185 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy186 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0188 :

nb078AlphaDummy183 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy182) (SemanticCore.Class.cv nb078AlphaDummy183)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy182) (SemanticCore.Class.cv nb078AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0189 (f : SemanticCore.Var) :

nb078AlphaDummy186 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy185 f)) (SemanticCore.Class.cv (nb078AlphaDummy186 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy185 f)) (SemanticCore.Class.cv (nb078AlphaDummy186 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0190 :

nb078AlphaDummy183 ∈ (SemanticCore.Class.cv nb078AlphaDummy182).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy183).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0191 (f : SemanticCore.Var) :

nb078AlphaDummy186 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy185 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy186 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0192 :

nb078AlphaDummy182 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy182)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0193 (f : SemanticCore.Var) :

nb078AlphaDummy185 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy185 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy186 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0194 :

nb078AlphaDummy182 ∈ (SemanticCore.Class.cv nb078AlphaDummy182).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy182).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0195 (f : SemanticCore.Var) :

nb078AlphaDummy185 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy185 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy185 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0196 :

nb078AlphaDummy183 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy182)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy183)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0197 (f : SemanticCore.Var) :

nb078AlphaDummy186 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy185 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy186 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0198 :

nb078AlphaDummy183 ∈ (SemanticCore.Class.cv nb078AlphaDummy183).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy183).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0199 (f : SemanticCore.Var) :

nb078AlphaDummy186 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy186 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy186 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0200 :

nb078AlphaDummy010 ∈ (SemanticCore.Class.cv nb078AlphaDummy011).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy010).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0201 :

nb078AlphaDummy010 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy168 (SemanticCore.Class.cv nb078AlphaDummy011) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy167) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy168 (SemanticCore.Class.cv nb078AlphaDummy010) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0202 (f : SemanticCore.Var) :

nb078AlphaDummy013 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy014 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy013 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0203 (f : SemanticCore.Var) :

nb078AlphaDummy013 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy170 f) (SemanticCore.Class.cv (nb078AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy170 f) (SemanticCore.Class.cv (nb078AlphaDummy013 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0204 :

nb078AlphaDummy010 ∈ (SemanticCore.Class.cab nb078AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy168 (SemanticCore.Class.cv nb078AlphaDummy010) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy167 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy168 (SemanticCore.Class.cv nb078AlphaDummy010) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0205 (f : SemanticCore.Var) :

nb078AlphaDummy013 f ∈ (SemanticCore.Class.cab (nb078AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy170 f) (SemanticCore.Class.cv (nb078AlphaDummy013 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy169 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy170 f) (SemanticCore.Class.cv (nb078AlphaDummy013 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0206 :

nb078AlphaDummy168 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0207 (f : SemanticCore.Var) :

nb078AlphaDummy170 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0208 :

nb078AlphaDummy168 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy168)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0209 (f : SemanticCore.Var) :

nb078AlphaDummy170 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy170 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0210 :

nb078AlphaDummy204 ∈ (SemanticCore.Class.cv nb078AlphaDummy204).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy203).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0211 :

nb078AlphaDummy204 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy207 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy208 (SemanticCore.Class.cv nb078AlphaDummy204) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy207) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy207 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy208 (SemanticCore.Class.cv nb078AlphaDummy203) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy207) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0212 (f : SemanticCore.Var) :

nb078AlphaDummy206 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy206 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy205 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0213 (f : SemanticCore.Var) :

nb078AlphaDummy206 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy209 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy210 f) (SemanticCore.Class.cv (nb078AlphaDummy206 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy209 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy209 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy210 f) (SemanticCore.Class.cv (nb078AlphaDummy205 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy209 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0215 (f : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0216 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0217 (f : SemanticCore.Var) :

nb078AlphaDummy210 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy210 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0218 :

nb078AlphaDummy215 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy215) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy215) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy215).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0220 :

nb078AlphaDummy215 ∈ (SemanticCore.Class.cv nb078AlphaDummy215).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0221 (f : SemanticCore.Var) :

nb078AlphaDummy217 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy217 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0222 :

nb078AlphaDummy222 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy222) (SemanticCore.Class.cv nb078AlphaDummy223)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy222) (SemanticCore.Class.cv nb078AlphaDummy223)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0223 (f : SemanticCore.Var) :

nb078AlphaDummy225 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy225 f)) (SemanticCore.Class.cv (nb078AlphaDummy226 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy225 f)) (SemanticCore.Class.cv (nb078AlphaDummy226 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0224 :

nb078AlphaDummy222 ∈ (SemanticCore.Class.cv nb078AlphaDummy222).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy223).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0225 (f : SemanticCore.Var) :

nb078AlphaDummy225 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy225 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy226 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0226 :

nb078AlphaDummy223 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy222) (SemanticCore.Class.cv nb078AlphaDummy223)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy222) (SemanticCore.Class.cv nb078AlphaDummy223)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0227 (f : SemanticCore.Var) :

nb078AlphaDummy226 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy225 f)) (SemanticCore.Class.cv (nb078AlphaDummy226 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy225 f)) (SemanticCore.Class.cv (nb078AlphaDummy226 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0228 :

nb078AlphaDummy223 ∈ (SemanticCore.Class.cv nb078AlphaDummy222).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy223).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0229 (f : SemanticCore.Var) :

nb078AlphaDummy226 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy225 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy226 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0230 :

nb078AlphaDummy222 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy222)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy223)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0231 (f : SemanticCore.Var) :

nb078AlphaDummy225 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy225 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy226 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0232 :

nb078AlphaDummy222 ∈ (SemanticCore.Class.cv nb078AlphaDummy222).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy222).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0233 (f : SemanticCore.Var) :

nb078AlphaDummy225 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy225 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy225 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0234 :

nb078AlphaDummy223 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy222)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy223)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0235 (f : SemanticCore.Var) :

nb078AlphaDummy226 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy225 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy226 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0236 :

nb078AlphaDummy223 ∈ (SemanticCore.Class.cv nb078AlphaDummy223).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy223).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0237 (f : SemanticCore.Var) :

nb078AlphaDummy226 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy226 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy226 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0238 :

nb078AlphaDummy203 ∈ (SemanticCore.Class.cv nb078AlphaDummy204).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy203).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0239 :

nb078AlphaDummy203 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy207 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy208 (SemanticCore.Class.cv nb078AlphaDummy204) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy207) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy207 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy208 (SemanticCore.Class.cv nb078AlphaDummy203) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy207) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0240 (f : SemanticCore.Var) :

nb078AlphaDummy205 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy206 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy205 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0241 (f : SemanticCore.Var) :

nb078AlphaDummy205 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy209 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy210 f) (SemanticCore.Class.cv (nb078AlphaDummy206 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy209 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy209 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy210 f) (SemanticCore.Class.cv (nb078AlphaDummy205 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy209 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0242 :

nb078AlphaDummy203 ∈ (SemanticCore.Class.cab nb078AlphaDummy207 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy208 (SemanticCore.Class.cv nb078AlphaDummy203) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy207) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy207 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy208 (SemanticCore.Class.cv nb078AlphaDummy203) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy207) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0243 (f : SemanticCore.Var) :

nb078AlphaDummy205 f ∈ (SemanticCore.Class.cab (nb078AlphaDummy209 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy210 f) (SemanticCore.Class.cv (nb078AlphaDummy205 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy209 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy209 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy210 f) (SemanticCore.Class.cv (nb078AlphaDummy205 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy209 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0244 :

nb078AlphaDummy208 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0245 (f : SemanticCore.Var) :

nb078AlphaDummy210 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0246 :

nb078AlphaDummy208 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy208)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0247 (f : SemanticCore.Var) :

nb078AlphaDummy210 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy210 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0248 :

nb078AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy000)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0249 (f : SemanticCore.Var) :

f ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0250 :

nb078AlphaDummy244 ∈ (SemanticCore.Class.cv nb078AlphaDummy244).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy243).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0251 :

nb078AlphaDummy244 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy247 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy248 (SemanticCore.Class.cv nb078AlphaDummy244) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy247) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy247 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy248 (SemanticCore.Class.cv nb078AlphaDummy243) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy247) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0252 (f : SemanticCore.Var) :

nb078AlphaDummy246 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy246 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy245 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0253 (f : SemanticCore.Var) :

nb078AlphaDummy246 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy249 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy250 f) (SemanticCore.Class.cv (nb078AlphaDummy246 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy249 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy249 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy250 f) (SemanticCore.Class.cv (nb078AlphaDummy245 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy249 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0255 (f : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0256 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0257 (f : SemanticCore.Var) :

nb078AlphaDummy250 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy250 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0258 :

nb078AlphaDummy255 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy255) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy255) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy255).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0260 :

nb078AlphaDummy255 ∈ (SemanticCore.Class.cv nb078AlphaDummy255).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0261 (f : SemanticCore.Var) :

nb078AlphaDummy257 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy257 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0262 :

nb078AlphaDummy262 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy262) (SemanticCore.Class.cv nb078AlphaDummy263)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy262) (SemanticCore.Class.cv nb078AlphaDummy263)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0263 (f : SemanticCore.Var) :

nb078AlphaDummy265 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy265 f)) (SemanticCore.Class.cv (nb078AlphaDummy266 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy265 f)) (SemanticCore.Class.cv (nb078AlphaDummy266 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0264 :

nb078AlphaDummy262 ∈ (SemanticCore.Class.cv nb078AlphaDummy262).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy263).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0265 (f : SemanticCore.Var) :

nb078AlphaDummy265 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy265 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy266 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0266 :

nb078AlphaDummy263 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy262) (SemanticCore.Class.cv nb078AlphaDummy263)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy262) (SemanticCore.Class.cv nb078AlphaDummy263)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0267 (f : SemanticCore.Var) :

nb078AlphaDummy266 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy265 f)) (SemanticCore.Class.cv (nb078AlphaDummy266 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy265 f)) (SemanticCore.Class.cv (nb078AlphaDummy266 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0268 :

nb078AlphaDummy263 ∈ (SemanticCore.Class.cv nb078AlphaDummy262).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy263).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0269 (f : SemanticCore.Var) :

nb078AlphaDummy266 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy265 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy266 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0270 :

nb078AlphaDummy262 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy262)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy263)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0271 (f : SemanticCore.Var) :

nb078AlphaDummy265 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy265 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy266 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0272 :

nb078AlphaDummy262 ∈ (SemanticCore.Class.cv nb078AlphaDummy262).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy262).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0273 (f : SemanticCore.Var) :

nb078AlphaDummy265 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy265 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy265 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0274 :

nb078AlphaDummy263 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy262)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy263)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0275 (f : SemanticCore.Var) :

nb078AlphaDummy266 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy265 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy266 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0276 :

nb078AlphaDummy263 ∈ (SemanticCore.Class.cv nb078AlphaDummy263).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy263).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0277 (f : SemanticCore.Var) :

nb078AlphaDummy266 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy266 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy266 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0278 :

nb078AlphaDummy243 ∈ (SemanticCore.Class.cv nb078AlphaDummy244).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy243).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0279 :

nb078AlphaDummy243 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy247 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy248 (SemanticCore.Class.cv nb078AlphaDummy244) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy247) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy247 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy248 (SemanticCore.Class.cv nb078AlphaDummy243) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy247) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0280 (f : SemanticCore.Var) :

nb078AlphaDummy245 f ∈ (SemanticCore.Class.cv (nb078AlphaDummy246 f)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy245 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0281 (f : SemanticCore.Var) :

nb078AlphaDummy245 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy249 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy250 f) (SemanticCore.Class.cv (nb078AlphaDummy246 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy249 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy249 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy250 f) (SemanticCore.Class.cv (nb078AlphaDummy245 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy249 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0282 :

nb078AlphaDummy243 ∈ (SemanticCore.Class.cab nb078AlphaDummy247 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy248 (SemanticCore.Class.cv nb078AlphaDummy243) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy247) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy247 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy248 (SemanticCore.Class.cv nb078AlphaDummy243) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy247) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0283 (f : SemanticCore.Var) :

nb078AlphaDummy245 f ∈ (SemanticCore.Class.cab (nb078AlphaDummy249 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy250 f) (SemanticCore.Class.cv (nb078AlphaDummy245 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy249 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy249 f) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy250 f) (SemanticCore.Class.cv (nb078AlphaDummy245 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy249 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0284 :

nb078AlphaDummy248 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0285 (f : SemanticCore.Var) :

nb078AlphaDummy250 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0286 :

nb078AlphaDummy248 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy248)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0287 (f : SemanticCore.Var) :

nb078AlphaDummy250 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy250 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0288 :

nb078AlphaDummy000 ∈ (SemanticCore.Class.cv nb078AlphaDummy000).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0289 (f : SemanticCore.Var) :

f ∈ (SemanticCore.Class.cv f).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0294 :

nb078AlphaDummy287 ∈ (SemanticCore.Class.cv nb078AlphaDummy287).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy288).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0295 :

nb078AlphaDummy287 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy295 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy296 (SemanticCore.Class.cv nb078AlphaDummy287) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy295) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy296)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy295 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy296 (SemanticCore.Class.cv nb078AlphaDummy288) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy295) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy296)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0296 (g : SemanticCore.Var) :

nb078AlphaDummy290 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy290 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy291 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0297 (g : SemanticCore.Var) :

nb078AlphaDummy290 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy297 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy298 g) (SemanticCore.Class.cv (nb078AlphaDummy290 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy297 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy297 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy298 g) (SemanticCore.Class.cv (nb078AlphaDummy291 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy297 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0299 (g : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0300 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0301 (g : SemanticCore.Var) :

nb078AlphaDummy298 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy298 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0302 :

nb078AlphaDummy303 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy303) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb078AlphaDummy303) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy303).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0304 :

nb078AlphaDummy303 ∈ (SemanticCore.Class.cv nb078AlphaDummy303).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0305 (g : SemanticCore.Var) :

nb078AlphaDummy305 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy305 g)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0306 :

nb078AlphaDummy310 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy310) (SemanticCore.Class.cv nb078AlphaDummy311)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy310) (SemanticCore.Class.cv nb078AlphaDummy311)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0307 (g : SemanticCore.Var) :

nb078AlphaDummy313 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy313 g)) (SemanticCore.Class.cv (nb078AlphaDummy314 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy313 g)) (SemanticCore.Class.cv (nb078AlphaDummy314 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0308 :

nb078AlphaDummy310 ∈ (SemanticCore.Class.cv nb078AlphaDummy310).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy311).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0309 (g : SemanticCore.Var) :

nb078AlphaDummy313 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy313 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy314 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0310 :

nb078AlphaDummy311 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy310) (SemanticCore.Class.cv nb078AlphaDummy311)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy310) (SemanticCore.Class.cv nb078AlphaDummy311)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0311 (g : SemanticCore.Var) :

nb078AlphaDummy314 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy313 g)) (SemanticCore.Class.cv (nb078AlphaDummy314 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy313 g)) (SemanticCore.Class.cv (nb078AlphaDummy314 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0312 :

nb078AlphaDummy311 ∈ (SemanticCore.Class.cv nb078AlphaDummy310).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy311).fv