NF weak partition development: NAR4H5C095M3Part005.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_789 (f : SemanticCore.Var) : nb095AlphaDummy207 f ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_790 (f : SemanticCore.Var) : nb095AlphaDummy208 f ∉ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_distinct_791 (f : SemanticCore.Var) : nb095AlphaDummy207 f ≠ nb095AlphaDummy208 f

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_792 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy249 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_fresh_793 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy250 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_distinct_794 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy249 D R S_cls E ≠ nb095AlphaDummy250 D R S_cls E

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_795 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb095AlphaDummy251 x R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv ∪ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_796 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb095AlphaDummy252 x R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv ∪ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_distinct_797 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb095AlphaDummy251 x R ≠ nb095AlphaDummy252 x R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_798 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy339 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_fresh_799 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy340 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_distinct_800 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy339 D R S_cls E ≠ nb095AlphaDummy340 D R S_cls E

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_801 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) : nb095AlphaDummy341 u S_cls ∉ (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_fresh_802 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) : nb095AlphaDummy342 u S_cls ∉ (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_distinct_803 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) : nb095AlphaDummy341 u S_cls ≠ nb095AlphaDummy342 u S_cls

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_804 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy009 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_fresh_805 (f : SemanticCore.Var) : nb095AlphaDummy010 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_fresh_806 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy383 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_807 (f : SemanticCore.Var) : nb095AlphaDummy384 f ∉ (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_808 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy023 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_fresh_809 (f : SemanticCore.Var) : nb095AlphaDummy024 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_fresh_810 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy059 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_fresh_811 (f : SemanticCore.Var) : nb095AlphaDummy060 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_fresh_812 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy101 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_fresh_813 (f : SemanticCore.Var) : nb095AlphaDummy102 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_fresh_814 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy137 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_fresh_815 (f : SemanticCore.Var) : nb095AlphaDummy138 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_fresh_816 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy173 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_fresh_817 (f : SemanticCore.Var) : nb095AlphaDummy174 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_fresh_818 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy213 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_fresh_819 (f : SemanticCore.Var) : nb095AlphaDummy214 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_fresh_820 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy259 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_fresh_821 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb095AlphaDummy260 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_fresh_822 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy303 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_fresh_823 (f : SemanticCore.Var) : nb095AlphaDummy304 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_fresh_824 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy349 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_fresh_825 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) : nb095AlphaDummy350 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_fresh_826 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy397 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy393 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy394 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy385 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy393 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy394 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy393 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy394 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy386 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy393 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy394 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_827 (f : SemanticCore.Var) : nb095AlphaDummy398 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy395 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy396 f) (SemanticCore.Class.cv (nb095AlphaDummy388 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy395 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy396 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy395 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy396 f) (SemanticCore.Class.cv (nb095AlphaDummy389 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy395 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy396 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_828 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy433 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy429 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy430 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy385 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy429 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy430 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy429 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy430 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy387 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy429 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy430 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_829 (f : SemanticCore.Var) : nb095AlphaDummy434 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy431 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy432 f) (SemanticCore.Class.cv (nb095AlphaDummy388 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy431 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy432 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy431 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy432 f) (SemanticCore.Class.cv (nb095AlphaDummy390 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy431 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy432 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_830 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy475 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy471 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy472 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy465 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy471 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy472 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy471 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy472 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy466 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy471 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy472 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_831 (f : SemanticCore.Var) : nb095AlphaDummy476 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy473 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy474 f) (SemanticCore.Class.cv (nb095AlphaDummy467 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy473 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy474 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy473 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy474 f) (SemanticCore.Class.cv (nb095AlphaDummy468 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy473 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy474 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_832 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy511 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy507 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy508 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy466 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy507 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy508 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy507 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy508 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy465 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy507 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy508 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_833 (f : SemanticCore.Var) : nb095AlphaDummy512 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy509 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy510 f) (SemanticCore.Class.cv (nb095AlphaDummy468 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy509 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy510 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy509 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy510 f) (SemanticCore.Class.cv (nb095AlphaDummy467 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy509 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy510 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_834 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy547 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy543 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy544 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy387 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy543 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy544 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy543 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy544 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy386 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy543 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy544 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_835 (f : SemanticCore.Var) : nb095AlphaDummy548 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy545 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy546 f) (SemanticCore.Class.cv (nb095AlphaDummy390 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy545 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy546 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy545 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy546 f) (SemanticCore.Class.cv (nb095AlphaDummy389 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy545 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy546 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_836 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy583 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy579 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy580 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy003 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy579 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy580 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy579 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy580 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy579 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy580 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_837 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy584 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy581 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy582 x u D R S_cls f E) (SemanticCore.Class.cv (nb095AlphaDummy005 x u D R S_cls f E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy581 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy582 x u D R S_cls f E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy581 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy582 x u D R S_cls f E) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy581 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy582 x u D R S_cls f E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_838 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy629 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy625 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy626 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy619 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy625 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy626 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy625 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy626 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy620 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy625 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy626 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_839 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy630 x D R ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy627 x D R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy628 x D R) (SemanticCore.Class.cv (nb095AlphaDummy621 x D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy627 x D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy628 x D R))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy627 x D R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy628 x D R) (SemanticCore.Class.cv (nb095AlphaDummy622 x D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy627 x D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy628 x D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_840 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy665 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy661 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy662 D R S_cls E) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy003 D R S_cls E))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy661 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy662 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy661 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy662 D R S_cls E) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy661 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy662 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_841 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy666 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy663 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy664 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy005 x u D R S_cls f E))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy663 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy664 x u D R S_cls f E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy663 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy664 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy663 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy664 x u D R S_cls f E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_842 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy681 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy677 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy678 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy003 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy677 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy678 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy677 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy678 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy669 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy677 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy678 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_843 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy682 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy679 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy680 x u D R S_cls f E) (SemanticCore.Class.cv (nb095AlphaDummy005 x u D R S_cls f E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy679 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy680 x u D R S_cls f E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy679 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy680 x u D R S_cls f E) (SemanticCore.Class.cv (nb095AlphaDummy670 x u D R S_cls f E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy679 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy680 x u D R S_cls f E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_844 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy751 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy747 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy748 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy747 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy748 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy747 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy748 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy739 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy747 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy748 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_845 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy752 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy749 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy750 x u D R S_cls f E) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy749 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy750 x u D R S_cls f E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy749 x u D R S_cls f E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy750 x u D R S_cls f E) (SemanticCore.Class.cv (nb095AlphaDummy740 x u D R S_cls f E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy749 x u D R S_cls f E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy750 x u D R S_cls f E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_846 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy803 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy799 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy800 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy793 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy799 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy800 D R S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy799 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy800 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy794 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy799 D R S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy800 D R S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_847 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy804 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy801 u S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy802 u S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy795 u S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy801 u S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy802 u S_cls E))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb095AlphaDummy801 u S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy802 u S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy796 u S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy801 u S_cls E)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy802 u S_cls E))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_848 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy043 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_fresh_849 (f : SemanticCore.Var) : nb095AlphaDummy044 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy037 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy038 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_850 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy079 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_fresh_851 (f : SemanticCore.Var) : nb095AlphaDummy080 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy073 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy074 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_852 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy121 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_fresh_853 (f : SemanticCore.Var) : nb095AlphaDummy122 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy115 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy116 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_854 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy157 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_fresh_855 (f : SemanticCore.Var) : nb095AlphaDummy158 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy151 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy152 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_856 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy193 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_fresh_857 (f : SemanticCore.Var) : nb095AlphaDummy194 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy187 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy188 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_858 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy233 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_fresh_859 (f : SemanticCore.Var) : nb095AlphaDummy234 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy227 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy228 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_860 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy279 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_fresh_861 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb095AlphaDummy280 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_fresh_862 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy323 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_fresh_863 (f : SemanticCore.Var) : nb095AlphaDummy324 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy317 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy318 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_864 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy369 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_fresh_865 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) : nb095AlphaDummy370 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_fresh_866 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy417 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy408 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy409 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_867 (f : SemanticCore.Var) : nb095AlphaDummy418 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy411 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy412 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_868 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy453 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy444 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy445 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_869 (f : SemanticCore.Var) : nb095AlphaDummy454 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy447 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy448 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_870 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy495 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy486 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy487 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_871 (f : SemanticCore.Var) : nb095AlphaDummy496 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy489 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy490 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_872 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy531 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy522 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy523 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_873 (f : SemanticCore.Var) : nb095AlphaDummy532 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy525 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy526 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_874 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy567 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy558 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy559 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_875 (f : SemanticCore.Var) : nb095AlphaDummy568 f ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy561 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy562 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_876 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy603 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy594 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy595 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_877 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy604 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy597 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy598 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_878 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy649 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy640 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy641 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_879 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy650 x D R ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy643 x D R))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy644 x D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_880 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy701 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy692 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy693 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_881 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy702 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy695 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy696 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_882 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy731 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy722 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy723 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_883 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy732 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy725 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy726 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_884 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy771 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy762 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy763 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_885 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy772 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy765 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy766 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_886 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy823 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy814 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy815 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_887 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy824 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy817 u S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb095AlphaDummy818 u S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_888 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy051 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_fresh_889 (f : SemanticCore.Var) : nb095AlphaDummy052 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_fresh_890 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy087 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_fresh_891 (f : SemanticCore.Var) : nb095AlphaDummy088 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_fresh_892 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy129 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_fresh_893 (f : SemanticCore.Var) : nb095AlphaDummy130 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_fresh_894 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy165 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_fresh_895 (f : SemanticCore.Var) : nb095AlphaDummy166 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_fresh_896 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy201 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_fresh_897 (f : SemanticCore.Var) : nb095AlphaDummy202 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_fresh_898 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy241 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_fresh_899 (f : SemanticCore.Var) : nb095AlphaDummy242 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_fresh_900 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy287 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_fresh_901 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb095AlphaDummy288 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_fresh_902 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy331 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_fresh_903 (f : SemanticCore.Var) : nb095AlphaDummy332 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_fresh_904 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy377 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_905 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) : nb095AlphaDummy378 u S_cls ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_906 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy425 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy394 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_907 (f : SemanticCore.Var) : nb095AlphaDummy426 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy396 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_908 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy461 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy430 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_909 (f : SemanticCore.Var) : nb095AlphaDummy462 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy432 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_910 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy503 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy472 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_911 (f : SemanticCore.Var) : nb095AlphaDummy504 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy474 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_912 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy539 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy508 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_913 (f : SemanticCore.Var) : nb095AlphaDummy540 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy510 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_914 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy575 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy544 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_915 (f : SemanticCore.Var) : nb095AlphaDummy576 f ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy546 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_916 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy611 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy580 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_917 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy612 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy582 x u D R S_cls f E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_918 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy657 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy626 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_919 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy658 x D R ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy628 x D R)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_920 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy785 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy662 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_921 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy786 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy664 x u D R S_cls f E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_922 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy709 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy678 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_923 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy710 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy680 x u D R S_cls f E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_924 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy779 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy748 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_925 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy780 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy750 x u D R S_cls f E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_926 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy831 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy800 D R S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_927 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy832 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy802 u S_cls E)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_928 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy661 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy003 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_929 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy662 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy003 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_distinct_930 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy661 D R S_cls E ≠ nb095AlphaDummy662 D R S_cls E

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_931 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy663 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy005 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_932 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy664 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy005 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_distinct_933 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy663 x u D R S_cls f E ≠ nb095AlphaDummy664 x u D R S_cls f E

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_934 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy619 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCin D (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 ∪ (Compiler.CompactSourceSyntax.synCin D (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_fresh_935 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy620 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCin D (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 ∪ (Compiler.CompactSourceSyntax.synCin D (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_distinct_936 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy619 D R S_cls E ≠ nb095AlphaDummy620 D R S_cls E

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_937 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy621 x D R ∉ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (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_fresh_938 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy622 x D R ∉ (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))).fv ∪ (Compiler.CompactSourceSyntax.synCin D (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_distinct_939 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy621 x D R ≠ nb095AlphaDummy622 x D R

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_940 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy793 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.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_fresh_941 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy794 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.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_distinct_942 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy793 D R S_cls E ≠ nb095AlphaDummy794 D R S_cls E

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_943 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy795 u 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 u)))).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_fresh_944 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy796 u 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 u)))).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_distinct_945 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy795 u S_cls E ≠ nb095AlphaDummy796 u S_cls E

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_946 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy039 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_fresh_947 (f : SemanticCore.Var) : nb095AlphaDummy040 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_fresh_948 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy075 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_fresh_949 (f : SemanticCore.Var) : nb095AlphaDummy076 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_fresh_950 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy117 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_fresh_951 (f : SemanticCore.Var) : nb095AlphaDummy118 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_fresh_952 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy153 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_fresh_953 (f : SemanticCore.Var) : nb095AlphaDummy154 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_fresh_954 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy189 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_fresh_955 (f : SemanticCore.Var) : nb095AlphaDummy190 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_fresh_956 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy229 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_fresh_957 (f : SemanticCore.Var) : nb095AlphaDummy230 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_fresh_958 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy275 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_fresh_959 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb095AlphaDummy276 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_fresh_960 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy319 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_fresh_961 (f : SemanticCore.Var) : nb095AlphaDummy320 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_fresh_962 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy365 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_fresh_963 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) : nb095AlphaDummy366 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_fresh_964 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy413 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy408 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy409 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy408 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy409 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_965 (f : SemanticCore.Var) : nb095AlphaDummy414 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy411 f)) (SemanticCore.Class.cv (nb095AlphaDummy412 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy411 f)) (SemanticCore.Class.cv (nb095AlphaDummy412 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_966 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy449 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy444 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy445 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy444 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy445 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_967 (f : SemanticCore.Var) : nb095AlphaDummy450 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy447 f)) (SemanticCore.Class.cv (nb095AlphaDummy448 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy447 f)) (SemanticCore.Class.cv (nb095AlphaDummy448 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_968 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy491 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy486 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy487 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy486 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy487 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_969 (f : SemanticCore.Var) : nb095AlphaDummy492 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy489 f)) (SemanticCore.Class.cv (nb095AlphaDummy490 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy489 f)) (SemanticCore.Class.cv (nb095AlphaDummy490 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_970 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy527 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy522 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy523 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy522 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy523 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_971 (f : SemanticCore.Var) : nb095AlphaDummy528 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy525 f)) (SemanticCore.Class.cv (nb095AlphaDummy526 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy525 f)) (SemanticCore.Class.cv (nb095AlphaDummy526 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_972 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy563 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy558 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy559 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy558 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy559 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_973 (f : SemanticCore.Var) : nb095AlphaDummy564 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy561 f)) (SemanticCore.Class.cv (nb095AlphaDummy562 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy561 f)) (SemanticCore.Class.cv (nb095AlphaDummy562 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_974 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy599 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy594 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy595 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy594 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy595 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_975 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy600 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy597 x u D R S_cls f E)) (SemanticCore.Class.cv (nb095AlphaDummy598 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy597 x u D R S_cls f E)) (SemanticCore.Class.cv (nb095AlphaDummy598 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_976 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy645 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy640 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy641 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy640 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy641 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_977 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy646 x D R ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy643 x D R)) (SemanticCore.Class.cv (nb095AlphaDummy644 x D R))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy643 x D R)) (SemanticCore.Class.cv (nb095AlphaDummy644 x D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_978 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy697 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy692 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy693 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy692 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy693 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_979 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy698 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy695 x u D R S_cls f E)) (SemanticCore.Class.cv (nb095AlphaDummy696 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy695 x u D R S_cls f E)) (SemanticCore.Class.cv (nb095AlphaDummy696 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_980 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy727 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy722 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy723 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy722 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy723 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_981 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy728 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy725 x u D R S_cls f E)) (SemanticCore.Class.cv (nb095AlphaDummy726 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy725 x u D R S_cls f E)) (SemanticCore.Class.cv (nb095AlphaDummy726 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_982 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy767 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy762 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy763 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy762 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy763 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_983 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy768 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy765 x u D R S_cls f E)) (SemanticCore.Class.cv (nb095AlphaDummy766 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy765 x u D R S_cls f E)) (SemanticCore.Class.cv (nb095AlphaDummy766 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_984 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy819 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy814 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy815 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy814 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy815 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_985 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy820 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy817 u S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy818 u S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb095AlphaDummy817 u S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy818 u S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_986 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy007 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)))) Compiler.CompactSourceSyntax.synCid).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_987 (f : SemanticCore.Var) : nb095AlphaDummy008 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_fresh_988 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy381 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))))) Compiler.CompactSourceSyntax.synCid).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_989 (f : SemanticCore.Var) : nb095AlphaDummy382 f ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) Compiler.CompactSourceSyntax.synCid).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_990 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy291 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_fresh_991 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy292 u S_cls f E ∉ (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_fresh_992 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy245 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin D (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 ∪ (Compiler.CompactSourceSyntax.synCnin D (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_fresh_993 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy246 x D R ∉ (Compiler.CompactSourceSyntax.synCnin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))).fv ∪ (Compiler.CompactSourceSyntax.synCnin D (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_fresh_994 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy335 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin 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 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_fresh_995 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy336 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin 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 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_fresh_996 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy615 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (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))))) (Compiler.CompactSourceSyntax.synCin D (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 ∪ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (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))))) (Compiler.CompactSourceSyntax.synCin D (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_fresh_997 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy616 x D R ∉ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))).fv ∪ (Compiler.CompactSourceSyntax.synCnin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (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_fresh_998 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy789 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin S_cls (Compiler.CompactSourceSyntax.synCxp (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))))) (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 S_cls (Compiler.CompactSourceSyntax.synCxp (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))))) (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_fresh_999 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy790 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCnin S_cls (Compiler.CompactSourceSyntax.synCxp (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)))) (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 S_cls (Compiler.CompactSourceSyntax.synCxp (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)))) (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_fresh_1000 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy053 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_fresh_1001 (f : SemanticCore.Var) : nb095AlphaDummy054 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy022 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy022 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1002 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy089 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_fresh_1003 (f : SemanticCore.Var) : nb095AlphaDummy090 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy058 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy058 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1004 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy131 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_fresh_1005 (f : SemanticCore.Var) : nb095AlphaDummy132 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy100 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1006 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy167 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_fresh_1007 (f : SemanticCore.Var) : nb095AlphaDummy168 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1008 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy203 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_fresh_1009 (f : SemanticCore.Var) : nb095AlphaDummy204 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1010 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy243 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_fresh_1011 (f : SemanticCore.Var) : nb095AlphaDummy244 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy212 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy212 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1012 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy289 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_fresh_1013 (x : SemanticCore.Var) (R : SemanticCore.Class) : nb095AlphaDummy290 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_fresh_1014 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy333 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_fresh_1015 (f : SemanticCore.Var) : nb095AlphaDummy334 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy302 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy302 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1016 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy379 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1017 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) : nb095AlphaDummy380 u S_cls ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1018 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy427 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy394 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy394 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1019 (f : SemanticCore.Var) : nb095AlphaDummy428 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy396 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy396 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1020 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy463 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy430 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy430 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1021 (f : SemanticCore.Var) : nb095AlphaDummy464 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy432 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy432 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1022 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy505 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy472 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy472 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1023 (f : SemanticCore.Var) : nb095AlphaDummy506 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy474 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy474 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1024 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy541 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy508 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy508 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1025 (f : SemanticCore.Var) : nb095AlphaDummy542 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy510 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy510 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1026 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy577 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy544 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy544 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1027 (f : SemanticCore.Var) : nb095AlphaDummy578 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy546 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy546 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1028 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy613 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy580 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy580 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1029 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy614 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy582 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy582 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1030 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy659 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy626 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy626 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1031 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy660 x D R ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy628 x D R))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy628 x D R))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1032 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy787 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy662 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy662 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1033 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy788 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy664 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy664 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1034 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy711 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy678 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy678 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1035 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy712 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy680 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy680 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1036 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy781 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy748 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy748 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1037 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy782 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy750 x u D R S_cls f E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy750 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1038 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy833 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy800 D R S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy800 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1039 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy834 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy802 u S_cls E))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy802 u S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1040 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy293 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_fresh_1041 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy294 u S_cls f E ∉ (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_fresh_1042 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy247 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_fresh_1043 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy248 x D R ∉ 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_fresh_1044 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy337 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_fresh_1045 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy338 u 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 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1046 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy617 D R S_cls E ∉ R.fv ∪ (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (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))))) (Compiler.CompactSourceSyntax.synCin D (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_fresh_1047 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy618 x D R ∉ R.fv ∪ (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (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_fresh_1048 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy000 D R S_cls E ∉ R.fv ∪ D.fv ∪ S_cls.fv ∪ E.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1049 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy001 D R S_cls E ∉ R.fv ∪ D.fv ∪ S_cls.fv ∪ E.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1050 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy002 D R S_cls E ∉ R.fv ∪ D.fv ∪ S_cls.fv ∪ E.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_distinct_1051 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy000 D R S_cls E ≠ nb095AlphaDummy001 D R S_cls E

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_distinct_1052 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy000 D R S_cls E ≠ nb095AlphaDummy002 D R S_cls E

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_distinct_1053 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy001 D R S_cls E ≠ nb095AlphaDummy002 D R S_cls E

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1054 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy791 D R S_cls E ∉ S_cls.fv ∪ (Compiler.CompactSourceSyntax.synCxp (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))))) (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_fresh_1055 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy792 u S_cls E ∉ S_cls.fv ∪ (Compiler.CompactSourceSyntax.synCxp (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)))) (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_fresh_1056 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy017 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_fresh_1057 (f : SemanticCore.Var) : nb095AlphaDummy018 f ∉ {nb095AlphaDummy014 f} ∪ {nb095AlphaDummy015 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb095AlphaDummy016 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy014 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb095AlphaDummy016 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy015 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1058 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy095 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_fresh_1059 (f : SemanticCore.Var) : nb095AlphaDummy096 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_fresh_1060 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy391 D R S_cls E ∉ {nb095AlphaDummy385 D R S_cls E} ∪ {nb095AlphaDummy386 D R S_cls E} ∪ (Compiler.CompactSourceSyntax.synWex (nb095AlphaDummy387 D R S_cls E) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy385 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)))) (SemanticCore.Class.cv (nb095AlphaDummy387 D R S_cls E))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy387 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (SemanticCore.Class.cv (nb095AlphaDummy386 D R S_cls E))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1061 (f : SemanticCore.Var) : nb095AlphaDummy392 f ∉ {nb095AlphaDummy388 f} ∪ {nb095AlphaDummy389 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb095AlphaDummy390 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy388 f)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) (SemanticCore.Class.cv (nb095AlphaDummy390 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy390 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb095AlphaDummy389 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1062 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy469 D R S_cls E ∉ {nb095AlphaDummy465 D R S_cls E} ∪ {nb095AlphaDummy466 D R S_cls E} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy466 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (SemanticCore.Class.cv (nb095AlphaDummy465 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1063 (f : SemanticCore.Var) : nb095AlphaDummy470 f ∉ {nb095AlphaDummy467 f} ∪ {nb095AlphaDummy468 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy468 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb095AlphaDummy467 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1064 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy623 D R S_cls E ∉ {nb095AlphaDummy619 D R S_cls E} ∪ {nb095AlphaDummy620 D R S_cls E} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy619 D R S_cls E)) (Compiler.CompactSourceSyntax.synCin D (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)))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy620 D R S_cls E)) (Compiler.CompactSourceSyntax.synCin D (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_fresh_1065 (x : SemanticCore.Var) (D R : SemanticCore.Class) : nb095AlphaDummy624 x D R ∉ {nb095AlphaDummy621 x D R} ∪ {nb095AlphaDummy622 x D R} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy621 x D R)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy622 x D R)) (Compiler.CompactSourceSyntax.synCin D (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_fresh_1066 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy671 D R S_cls E ∉ {nb095AlphaDummy669 D R S_cls E} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy003 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy669 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1067 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy672 x u D R S_cls f E ∉ {nb095AlphaDummy670 x u D R S_cls f E} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy005 x u D R S_cls f E)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy670 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1068 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy741 D R S_cls E ∉ {nb095AlphaDummy739 D R S_cls E} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy004 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy739 D R S_cls E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1069 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy742 x u D R S_cls f E ∉ {nb095AlphaDummy740 x u D R S_cls f E} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy006 x u D R S_cls f E)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy740 x u D R S_cls f E))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_fresh_1070 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy797 D R S_cls E ∉ {nb095AlphaDummy793 D R S_cls E} ∪ {nb095AlphaDummy794 D R S_cls E} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy793 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)))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy794 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_fresh_1071 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy798 u S_cls E ∉ {nb095AlphaDummy795 u S_cls E} ∪ {nb095AlphaDummy796 u S_cls E} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy795 u 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 u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy796 u 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 u)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0000 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy011 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_0001 (f : SemanticCore.Var) : nb095AlphaDummy014 f ∈ {nb095AlphaDummy014 f} ∪ {nb095AlphaDummy015 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb095AlphaDummy016 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy014 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb095AlphaDummy016 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy015 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0002 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy012 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_0003 (f : SemanticCore.Var) : nb095AlphaDummy015 f ∈ {nb095AlphaDummy014 f} ∪ {nb095AlphaDummy015 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb095AlphaDummy016 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy014 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb095AlphaDummy016 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy015 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0004 (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 (nb095AlphaDummy012 D R S_cls E)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_support_mem_0005 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy011 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_0006 (f : SemanticCore.Var) : nb095AlphaDummy014 f ∈ (SemanticCore.Class.cv (nb095AlphaDummy014 f)).fv ∪ (SemanticCore.Class.cv (nb095AlphaDummy015 f)).fv