Documentation

LeanPool.NFWeakPartition.NAR4H5C095M3Part006

NF weak partition development: NAR4H5C095M3Part006.

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

nb095AlphaDummy014 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy021 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy022 f) (SemanticCore.Class.cv (nb095AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy021 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy022 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy021 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy022 f) (SemanticCore.Class.cv (nb095AlphaDummy015 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy021 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy022 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0008 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy011 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy019 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy020 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy019 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy020 D R S_cls E)))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy019 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy020 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy019 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy020 D R S_cls E)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0010 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy020 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy020 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0012 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy027 D R S_cls E ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy027 D R S_cls E)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb095AlphaDummy027 D R S_cls E)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy027 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0014 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy027 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy027 D R S_cls E)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0016 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy034 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy034 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy035 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy034 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy035 D R S_cls E))).fv

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

nb095AlphaDummy037 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy037 f)) (SemanticCore.Class.cv (nb095AlphaDummy038 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy037 f)) (SemanticCore.Class.cv (nb095AlphaDummy038 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0018 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy034 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy034 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy035 D R S_cls E)).fv

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

nb095AlphaDummy037 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy037 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy038 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0020 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy035 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy034 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy035 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy034 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy035 D R S_cls E))).fv

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

nb095AlphaDummy038 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy037 f)) (SemanticCore.Class.cv (nb095AlphaDummy038 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy037 f)) (SemanticCore.Class.cv (nb095AlphaDummy038 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0022 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy035 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy034 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy035 D R S_cls E)).fv

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

nb095AlphaDummy038 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy037 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy038 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0024 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy034 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy034 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy035 D R S_cls E))).fv

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

nb095AlphaDummy037 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy037 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy038 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0026 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy034 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy034 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy034 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0028 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy035 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy034 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy035 D R S_cls E))).fv

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

nb095AlphaDummy038 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy037 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy038 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0030 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy035 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy035 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy035 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0032 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy012 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0033 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy012 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy019 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy020 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy019 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy020 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy019 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy020 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy019 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy020 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy015 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy014 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy015 f)).fv

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

nb095AlphaDummy015 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy021 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy022 f) (SemanticCore.Class.cv (nb095AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy021 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy022 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy021 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy022 f) (SemanticCore.Class.cv (nb095AlphaDummy015 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy021 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy022 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0036 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy012 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy019 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy020 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy019 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy020 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy019 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy020 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy019 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy020 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb095AlphaDummy015 f ∈ (SemanticCore.Class.cab (nb095AlphaDummy021 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy022 f) (SemanticCore.Class.cv (nb095AlphaDummy015 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy021 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy022 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy021 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy022 f) (SemanticCore.Class.cv (nb095AlphaDummy015 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy021 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy022 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0038 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy020 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy020 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0040 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy020 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy020 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy020 D R S_cls E))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0042 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy011 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0043 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy011 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy055 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy056 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy055 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy055 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy056 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy055 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy014 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy014 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy016 f)).fv

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

nb095AlphaDummy014 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy057 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy058 f) (SemanticCore.Class.cv (nb095AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy057 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy058 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy057 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy058 f) (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy057 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy058 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0046 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy011 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy055 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy056 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy055 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E)))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy055 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy056 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy055 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0048 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy056 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0050 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy063 D R S_cls E ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy063 D R S_cls E)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb095AlphaDummy063 D R S_cls E)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy063 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0052 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy063 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy063 D R S_cls E)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0054 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy070 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy070 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy071 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy070 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy071 D R S_cls E))).fv

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

nb095AlphaDummy073 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy073 f)) (SemanticCore.Class.cv (nb095AlphaDummy074 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy073 f)) (SemanticCore.Class.cv (nb095AlphaDummy074 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0056 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy070 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy070 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy071 D R S_cls E)).fv

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

nb095AlphaDummy073 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy073 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy074 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0058 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy071 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy070 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy071 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy070 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy071 D R S_cls E))).fv

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

nb095AlphaDummy074 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy073 f)) (SemanticCore.Class.cv (nb095AlphaDummy074 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy073 f)) (SemanticCore.Class.cv (nb095AlphaDummy074 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0060 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy071 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy070 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy071 D R S_cls E)).fv

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

nb095AlphaDummy074 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy073 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy074 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0062 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy070 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy070 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy071 D R S_cls E))).fv

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

nb095AlphaDummy073 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy073 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy074 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0064 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy070 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy070 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy070 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0066 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy071 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy070 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy071 D R S_cls E))).fv

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

nb095AlphaDummy074 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy073 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy074 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0068 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy071 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy071 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy071 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0070 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy013 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0071 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy013 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy055 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy056 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy055 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy055 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy056 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy055 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy016 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy014 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy016 f)).fv

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

nb095AlphaDummy016 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy057 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy058 f) (SemanticCore.Class.cv (nb095AlphaDummy014 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy057 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy058 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy057 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy058 f) (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy057 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy058 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0074 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy013 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy055 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy056 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy055 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy055 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy056 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy055 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb095AlphaDummy016 f ∈ (SemanticCore.Class.cab (nb095AlphaDummy057 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy058 f) (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy057 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy058 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy057 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy058 f) (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy057 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy058 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0076 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy056 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0078 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy056 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy056 D R S_cls E))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0080 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy091 D R S_cls E ∈ {nb095AlphaDummy091 D R S_cls E} ∪ {nb095AlphaDummy092 D R S_cls E} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0082 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy092 D R S_cls E ∈ {nb095AlphaDummy091 D R S_cls E} ∪ {nb095AlphaDummy092 D R S_cls E} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0084 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy091 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0085 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy091 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy097 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy098 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy097 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy097 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy098 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy097 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy093 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy093 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy094 f)).fv

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

nb095AlphaDummy093 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy099 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy100 f) (SemanticCore.Class.cv (nb095AlphaDummy093 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy099 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy099 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy100 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy099 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0088 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy091 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy097 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy098 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy097 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E)))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy097 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy098 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy097 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0090 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy098 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0092 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy105 D R S_cls E ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy105 D R S_cls E)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb095AlphaDummy105 D R S_cls E)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy105 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0094 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy105 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy105 D R S_cls E)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0096 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy112 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy112 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy113 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy112 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy113 D R S_cls E))).fv

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

nb095AlphaDummy115 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy115 f)) (SemanticCore.Class.cv (nb095AlphaDummy116 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy115 f)) (SemanticCore.Class.cv (nb095AlphaDummy116 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0098 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy112 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy112 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy113 D R S_cls E)).fv

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

nb095AlphaDummy115 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy115 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy116 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0100 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy113 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy112 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy113 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy112 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy113 D R S_cls E))).fv

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

nb095AlphaDummy116 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy115 f)) (SemanticCore.Class.cv (nb095AlphaDummy116 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy115 f)) (SemanticCore.Class.cv (nb095AlphaDummy116 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0102 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy113 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy112 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy113 D R S_cls E)).fv

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

nb095AlphaDummy116 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy115 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy116 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0104 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy112 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy112 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy113 D R S_cls E))).fv

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

nb095AlphaDummy115 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy115 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy116 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0106 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy112 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy112 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy112 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0108 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy113 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy112 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy113 D R S_cls E))).fv

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

nb095AlphaDummy116 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy115 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy116 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0110 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy113 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy113 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy113 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0112 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy092 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0113 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy092 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy097 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy098 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy097 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy097 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy098 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy097 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy094 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy093 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy094 f)).fv

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

nb095AlphaDummy094 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy099 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy100 f) (SemanticCore.Class.cv (nb095AlphaDummy093 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy099 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy099 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy100 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy099 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0116 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy092 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy097 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy098 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy097 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy097 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy098 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy097 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb095AlphaDummy094 f ∈ (SemanticCore.Class.cab (nb095AlphaDummy099 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy100 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy099 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy099 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy100 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy099 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0118 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy098 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0120 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy098 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy098 D R S_cls E))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0122 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy092 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0123 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy092 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy094 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy094 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy093 f)).fv

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

nb095AlphaDummy094 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy135 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy135 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy093 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0126 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy092 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E)))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0128 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy134 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0130 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy141 D R S_cls E ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy141 D R S_cls E)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb095AlphaDummy141 D R S_cls E)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy141 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0132 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy141 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy141 D R S_cls E)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0134 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy148 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy148 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy149 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy148 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy149 D R S_cls E))).fv

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

nb095AlphaDummy151 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy151 f)) (SemanticCore.Class.cv (nb095AlphaDummy152 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy151 f)) (SemanticCore.Class.cv (nb095AlphaDummy152 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0136 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy148 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy148 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy149 D R S_cls E)).fv

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

nb095AlphaDummy151 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy151 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy152 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0138 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy149 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy148 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy149 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy148 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy149 D R S_cls E))).fv

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

nb095AlphaDummy152 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy151 f)) (SemanticCore.Class.cv (nb095AlphaDummy152 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy151 f)) (SemanticCore.Class.cv (nb095AlphaDummy152 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0140 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy149 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy148 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy149 D R S_cls E)).fv

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

nb095AlphaDummy152 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy151 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy152 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0142 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy148 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy148 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy149 D R S_cls E))).fv

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

nb095AlphaDummy151 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy151 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy152 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0144 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy148 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy148 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy148 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0146 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy149 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy148 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy149 D R S_cls E))).fv

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

nb095AlphaDummy152 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy151 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy152 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0148 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy149 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy149 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy149 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0150 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy091 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0151 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy091 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy093 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy094 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy093 f)).fv

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

nb095AlphaDummy093 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy135 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy135 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy093 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0154 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy091 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb095AlphaDummy093 f ∈ (SemanticCore.Class.cab (nb095AlphaDummy135 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy093 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy135 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy093 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0156 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy134 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0158 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy134 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_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.nb095_support_mem_0162 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy000 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_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.nb095_support_mem_0164 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy000 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0165 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy000 D R S_cls E ∈ {nb095AlphaDummy011 D R S_cls E} ∪ {nb095AlphaDummy012 D R S_cls E} ∪ (Compiler.CompactSourceSyntax.synWex (nb095AlphaDummy013 D R S_cls E) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E))))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0168 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy000 D R S_cls E ∈ {nb095AlphaDummy091 D R S_cls E} ∪ {nb095AlphaDummy092 D R S_cls E} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy091 D R S_cls E))).fv

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

f ∈ {nb095AlphaDummy093 f} ∪ {nb095AlphaDummy094 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy094 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy093 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0170 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy000 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0172 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy013 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0173 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy013 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy016 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy016 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy015 f)).fv

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

nb095AlphaDummy016 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy172 f) (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy172 f) (SemanticCore.Class.cv (nb095AlphaDummy015 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0176 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy013 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E)))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0178 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy170 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0180 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy177 D R S_cls E ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy177 D R S_cls E)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb095AlphaDummy177 D R S_cls E)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy177 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0182 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy177 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy177 D R S_cls E)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0184 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy184 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy184 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy185 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy184 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy185 D R S_cls E))).fv

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

nb095AlphaDummy187 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy187 f)) (SemanticCore.Class.cv (nb095AlphaDummy188 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy187 f)) (SemanticCore.Class.cv (nb095AlphaDummy188 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0186 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy184 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy184 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy185 D R S_cls E)).fv

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

nb095AlphaDummy187 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy187 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy188 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0188 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy185 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy184 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy185 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy184 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy185 D R S_cls E))).fv

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

nb095AlphaDummy188 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy187 f)) (SemanticCore.Class.cv (nb095AlphaDummy188 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy187 f)) (SemanticCore.Class.cv (nb095AlphaDummy188 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0190 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy185 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy184 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy185 D R S_cls E)).fv

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

nb095AlphaDummy188 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy187 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy188 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0192 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy184 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy184 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy185 D R S_cls E))).fv

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

nb095AlphaDummy187 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy187 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy188 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0194 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy184 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy184 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy184 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0196 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy185 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy184 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy185 D R S_cls E))).fv

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

nb095AlphaDummy188 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy187 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy188 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0198 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy185 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy185 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy185 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0200 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy012 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0201 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy012 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy015 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy016 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy015 f)).fv

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

nb095AlphaDummy015 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy172 f) (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy172 f) (SemanticCore.Class.cv (nb095AlphaDummy015 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0204 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy012 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb095AlphaDummy015 f ∈ (SemanticCore.Class.cab (nb095AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy172 f) (SemanticCore.Class.cv (nb095AlphaDummy015 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy172 f) (SemanticCore.Class.cv (nb095AlphaDummy015 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0206 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy170 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0208 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy170 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0210 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy206 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy206 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy205 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0211 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy206 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy209 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy210 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy206 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy209 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy209 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy210 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy205 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy209 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy208 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy208 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy207 f)).fv

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

nb095AlphaDummy208 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy211 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy212 f) (SemanticCore.Class.cv (nb095AlphaDummy208 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy211 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy212 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy211 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy212 f) (SemanticCore.Class.cv (nb095AlphaDummy207 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy211 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy212 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0214 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy206 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy209 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy210 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy206 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy209 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E)))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy209 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy210 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy206 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy209 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0216 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy210 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0218 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy217 D R S_cls E ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy217 D R S_cls E)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb095AlphaDummy217 D R S_cls E)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy217 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0220 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy217 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy217 D R S_cls E)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0222 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy224 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy224 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy225 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy224 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy225 D R S_cls E))).fv

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

nb095AlphaDummy227 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy227 f)) (SemanticCore.Class.cv (nb095AlphaDummy228 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy227 f)) (SemanticCore.Class.cv (nb095AlphaDummy228 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0224 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy224 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy224 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy225 D R S_cls E)).fv

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

nb095AlphaDummy227 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy227 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy228 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0226 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy225 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy224 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy225 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy224 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy225 D R S_cls E))).fv

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

nb095AlphaDummy228 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy227 f)) (SemanticCore.Class.cv (nb095AlphaDummy228 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy227 f)) (SemanticCore.Class.cv (nb095AlphaDummy228 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0228 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy225 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy224 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy225 D R S_cls E)).fv

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

nb095AlphaDummy228 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy227 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy228 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0230 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy224 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy224 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy225 D R S_cls E))).fv

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

nb095AlphaDummy227 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy227 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy228 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0232 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy224 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy224 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy224 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0234 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy225 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy224 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy225 D R S_cls E))).fv

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

nb095AlphaDummy228 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy227 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy228 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0236 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy225 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy225 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy225 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0238 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy205 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy206 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy205 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0239 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy205 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy209 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy210 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy206 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy209 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy209 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy210 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy205 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy209 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy207 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy208 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy207 f)).fv

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

nb095AlphaDummy207 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy211 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy212 f) (SemanticCore.Class.cv (nb095AlphaDummy208 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy211 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy212 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy211 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy212 f) (SemanticCore.Class.cv (nb095AlphaDummy207 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy211 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy212 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0242 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy205 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy209 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy210 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy205 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy209 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy209 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy210 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy205 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy209 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb095AlphaDummy207 f ∈ (SemanticCore.Class.cab (nb095AlphaDummy211 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy212 f) (SemanticCore.Class.cv (nb095AlphaDummy207 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy211 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy212 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy211 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy212 f) (SemanticCore.Class.cv (nb095AlphaDummy207 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy211 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy212 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0244 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy210 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0246 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy210 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy210 D R S_cls E))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0248 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy000 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0252 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy002 D R S_cls E ∈ D.fv ∪ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy002 D R S_cls E)))).fv

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

x ∈ D.fv ∪ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0254 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy002 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv ∪ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy002 D R S_cls E))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0256 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy002 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy002 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0258 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy250 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy250 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy249 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0259 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy250 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy250 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy249 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy252 x R ∈ (SemanticCore.Class.cv (nb095AlphaDummy252 x R)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy251 x R)).fv

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

nb095AlphaDummy252 x R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy257 x R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy258 x R) (SemanticCore.Class.cv (nb095AlphaDummy252 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy257 x R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy257 x R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy258 x R) (SemanticCore.Class.cv (nb095AlphaDummy251 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy257 x R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0262 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy250 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy250 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E)))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy250 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0264 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy256 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0266 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy263 D R S_cls E ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy263 D R S_cls E)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb095AlphaDummy263 D R S_cls E)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy263 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0268 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy263 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy263 D R S_cls E)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0270 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy270 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy270 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy271 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy270 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy271 D R S_cls E))).fv

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

nb095AlphaDummy273 x R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy273 x R)) (SemanticCore.Class.cv (nb095AlphaDummy274 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy273 x R)) (SemanticCore.Class.cv (nb095AlphaDummy274 x R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0272 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy270 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy270 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy271 D R S_cls E)).fv

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

nb095AlphaDummy273 x R ∈ (SemanticCore.Class.cv (nb095AlphaDummy273 x R)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy274 x R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0274 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy271 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy270 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy271 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy270 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy271 D R S_cls E))).fv

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

nb095AlphaDummy274 x R ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy273 x R)) (SemanticCore.Class.cv (nb095AlphaDummy274 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy273 x R)) (SemanticCore.Class.cv (nb095AlphaDummy274 x R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0276 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy271 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy270 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy271 D R S_cls E)).fv

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

nb095AlphaDummy274 x R ∈ (SemanticCore.Class.cv (nb095AlphaDummy273 x R)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy274 x R)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0278 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy270 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy270 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy271 D R S_cls E))).fv

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

nb095AlphaDummy273 x R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy273 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy274 x R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0280 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy270 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy270 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy270 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0282 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy271 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy270 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy271 D R S_cls E))).fv

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

nb095AlphaDummy274 x R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy273 x R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy274 x R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0284 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy271 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy271 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy271 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0286 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy249 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy250 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy249 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0287 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy249 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy250 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy249 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy251 x R ∈ (SemanticCore.Class.cv (nb095AlphaDummy252 x R)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy251 x R)).fv

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

nb095AlphaDummy251 x R ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy257 x R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy258 x R) (SemanticCore.Class.cv (nb095AlphaDummy252 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy257 x R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy257 x R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy258 x R) (SemanticCore.Class.cv (nb095AlphaDummy251 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy257 x R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0290 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy249 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy249 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy249 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb095AlphaDummy251 x R ∈ (SemanticCore.Class.cab (nb095AlphaDummy257 x R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy258 x R) (SemanticCore.Class.cv (nb095AlphaDummy251 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy257 x R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy257 x R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy258 x R) (SemanticCore.Class.cv (nb095AlphaDummy251 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy257 x R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0292 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy256 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0294 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy256 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0296 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy296 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy296 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy295 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0297 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy296 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy299 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy300 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy296 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy299 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy299 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy300 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy295 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy299 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy298 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy298 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy297 f)).fv

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

nb095AlphaDummy298 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy301 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy302 f) (SemanticCore.Class.cv (nb095AlphaDummy298 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy301 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy302 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy301 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy302 f) (SemanticCore.Class.cv (nb095AlphaDummy297 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy301 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy302 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0300 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy296 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy299 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy300 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy296 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy299 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E)))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy299 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy300 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy296 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy299 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0302 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy300 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0304 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy307 D R S_cls E ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy307 D R S_cls E)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb095AlphaDummy307 D R S_cls E)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy307 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0306 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy307 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy307 D R S_cls E)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0308 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy314 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy314 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy315 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy314 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy315 D R S_cls E))).fv

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

nb095AlphaDummy317 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy317 f)) (SemanticCore.Class.cv (nb095AlphaDummy318 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy317 f)) (SemanticCore.Class.cv (nb095AlphaDummy318 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0310 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy314 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy314 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy315 D R S_cls E)).fv

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

nb095AlphaDummy317 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy317 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy318 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0312 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy315 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy314 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy315 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy314 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy315 D R S_cls E))).fv

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

nb095AlphaDummy318 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy317 f)) (SemanticCore.Class.cv (nb095AlphaDummy318 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy317 f)) (SemanticCore.Class.cv (nb095AlphaDummy318 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0314 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy315 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy314 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy315 D R S_cls E)).fv

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

nb095AlphaDummy318 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy317 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy318 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0316 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy314 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy314 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy315 D R S_cls E))).fv

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

nb095AlphaDummy317 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy317 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy318 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0318 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy314 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy314 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy314 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0320 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy315 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy314 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy315 D R S_cls E))).fv

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

nb095AlphaDummy318 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy317 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy318 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0322 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy315 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy315 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy315 D R S_cls E)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0324 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy295 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy296 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy295 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0325 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy295 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy299 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy300 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy296 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy299 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy299 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy300 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy295 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy299 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb095AlphaDummy297 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy298 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy297 f)).fv

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

nb095AlphaDummy297 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy301 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy302 f) (SemanticCore.Class.cv (nb095AlphaDummy298 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy301 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy302 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy301 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy302 f) (SemanticCore.Class.cv (nb095AlphaDummy297 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy301 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy302 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0328 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy295 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy299 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy300 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy295 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy299 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy299 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy300 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy295 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy299 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb095AlphaDummy297 f ∈ (SemanticCore.Class.cab (nb095AlphaDummy301 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy302 f) (SemanticCore.Class.cv (nb095AlphaDummy297 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy301 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy302 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy301 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy302 f) (SemanticCore.Class.cv (nb095AlphaDummy297 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy301 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy302 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0330 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy300 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0332 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy300 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy300 D R S_cls E))).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0334 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy000 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E)))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0335 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :

f ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0336 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy000 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0337 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :

f ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)).fv ∪ (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0338 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy000 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0340 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy001 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E)))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0341 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :

u ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0342 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy001 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0343 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) :

u ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)).fv ∪ (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0344 (D R S_cls E : SemanticCore.Class) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0346 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy001 D R S_cls E ∈ E.fv ∪ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0347 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) :

u ∈ E.fv ∪ (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0348 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy001 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv ∪ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0349 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

u ∈ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv ∪ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0350 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy001 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy001 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0351 (u : SemanticCore.Var) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0352 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy340 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy340 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy339 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0353 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy340 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy345 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy346 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy340 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy345 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy345 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy346 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy339 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy345 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0354 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy342 u S_cls ∈ (SemanticCore.Class.cv (nb095AlphaDummy342 u S_cls)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy341 u S_cls)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0355 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy342 u S_cls ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy347 u S_cls) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy348 u S_cls) (SemanticCore.Class.cv (nb095AlphaDummy342 u S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy347 u S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy347 u S_cls) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy348 u S_cls) (SemanticCore.Class.cv (nb095AlphaDummy341 u S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy347 u S_cls)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0356 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy340 D R S_cls E ∈ (SemanticCore.Class.cab (nb095AlphaDummy345 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy346 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy340 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy345 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E)))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy345 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy346 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy340 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy345 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0357 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy342 u S_cls ∈ (SemanticCore.Class.cab (nb095AlphaDummy347 u S_cls) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy348 u S_cls) (SemanticCore.Class.cv (nb095AlphaDummy342 u S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy347 u S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls)))))).fv ∪ (SemanticCore.Class.cab (nb095AlphaDummy347 u S_cls) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy348 u S_cls) (SemanticCore.Class.cv (nb095AlphaDummy342 u S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy347 u S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0358 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy346 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0359 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy348 u S_cls ∈ (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0360 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy353 D R S_cls E ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy353 D R S_cls E)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb095AlphaDummy353 D R S_cls E)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy353 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0362 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy353 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy353 D R S_cls E)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0363 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy355 u S_cls ∈ (SemanticCore.Class.cv (nb095AlphaDummy355 u S_cls)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0364 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy360 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy360 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy361 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy360 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy361 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0365 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy363 u S_cls ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy363 u S_cls)) (SemanticCore.Class.cv (nb095AlphaDummy364 u S_cls))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy363 u S_cls)) (SemanticCore.Class.cv (nb095AlphaDummy364 u S_cls))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0366 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy360 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy360 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy361 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0367 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy363 u S_cls ∈ (SemanticCore.Class.cv (nb095AlphaDummy363 u S_cls)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy364 u S_cls)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0368 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy361 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy360 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy361 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy360 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy361 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0369 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy364 u S_cls ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy363 u S_cls)) (SemanticCore.Class.cv (nb095AlphaDummy364 u S_cls))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy363 u S_cls)) (SemanticCore.Class.cv (nb095AlphaDummy364 u S_cls))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0370 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy361 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy360 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy361 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0371 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy364 u S_cls ∈ (SemanticCore.Class.cv (nb095AlphaDummy363 u S_cls)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy364 u S_cls)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0372 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy360 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy360 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy361 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0373 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy363 u S_cls ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy363 u S_cls))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy364 u S_cls))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0374 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy360 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy360 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy360 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0375 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy363 u S_cls ∈ (SemanticCore.Class.cv (nb095AlphaDummy363 u S_cls)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy363 u S_cls)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0376 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy361 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy360 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy361 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0377 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy364 u S_cls ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy363 u S_cls))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy364 u S_cls))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0378 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy361 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy361 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy361 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0379 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy364 u S_cls ∈ (SemanticCore.Class.cv (nb095AlphaDummy364 u S_cls)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy364 u S_cls)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0380 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy339 D R S_cls E ∈ (SemanticCore.Class.cv (nb095AlphaDummy340 D R S_cls E)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy339 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0381 (D R S_cls E : SemanticCore.Class) :

nb095AlphaDummy339 D R S_cls E ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy345 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy346 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy340 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy345 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy345 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy346 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy339 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy345 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0382 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy341 u S_cls ∈ (SemanticCore.Class.cv (nb095AlphaDummy342 u S_cls)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy341 u S_cls)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0383 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) :

nb095AlphaDummy341 u S_cls ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy347 u S_cls) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy348 u S_cls) (SemanticCore.Class.cv (nb095AlphaDummy342 u S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy347 u S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy347 u S_cls) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy348 u S_cls) (SemanticCore.Class.cv (nb095AlphaDummy341 u S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy347 u S_cls)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv