Nominal proof certificates grouped in dependency order.

Certificates from NAR4C057C001Part005.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_322 : nb057AlphaDummy072 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy067) (SemanticCore.Class.cv nb057AlphaDummy068)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy067) (SemanticCore.Class.cv nb057AlphaDummy068)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_323 (f : SemanticCore.Var) : nb057AlphaDummy073 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy070 f)) (SemanticCore.Class.cv (nb057AlphaDummy071 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy070 f)) (SemanticCore.Class.cv (nb057AlphaDummy071 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_324 : nb057AlphaDummy108 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy103) (SemanticCore.Class.cv nb057AlphaDummy104)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy103) (SemanticCore.Class.cv nb057AlphaDummy104)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_325 (f : SemanticCore.Var) : nb057AlphaDummy109 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy106 f)) (SemanticCore.Class.cv (nb057AlphaDummy107 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy106 f)) (SemanticCore.Class.cv (nb057AlphaDummy107 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_326 : nb057AlphaDummy150 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_327 (f : SemanticCore.Var) : nb057AlphaDummy151 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_328 : nb057AlphaDummy186 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_329 (f : SemanticCore.Var) : nb057AlphaDummy187 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_330 : nb057AlphaDummy222 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy217) (SemanticCore.Class.cv nb057AlphaDummy218)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy217) (SemanticCore.Class.cv nb057AlphaDummy218)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_331 (f : SemanticCore.Var) : nb057AlphaDummy223 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy220 f)) (SemanticCore.Class.cv (nb057AlphaDummy221 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy220 f)) (SemanticCore.Class.cv (nb057AlphaDummy221 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_332 : nb057AlphaDummy262 ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy257) (SemanticCore.Class.cv nb057AlphaDummy258)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy257) (SemanticCore.Class.cv nb057AlphaDummy258)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_333 (f : SemanticCore.Var) : nb057AlphaDummy263 f ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy260 f)) (SemanticCore.Class.cv (nb057AlphaDummy261 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy260 f)) (SemanticCore.Class.cv (nb057AlphaDummy261 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_334 : nb057AlphaDummy040 ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb057AlphaDummy001) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb057AlphaDummy001) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001))) Compiler.CompactSourceSyntax.synCid).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_335 (f : SemanticCore.Var) : nb057AlphaDummy041 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.nb057_fresh_336 : nb057AlphaDummy038 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_337 (f a : SemanticCore.Var) : nb057AlphaDummy039 f a ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_338 : nb057AlphaDummy086 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_339 (f : SemanticCore.Var) : nb057AlphaDummy087 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_340 : nb057AlphaDummy122 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_341 (f : SemanticCore.Var) : nb057AlphaDummy123 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_342 : nb057AlphaDummy164 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_343 (f : SemanticCore.Var) : nb057AlphaDummy165 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_344 : nb057AlphaDummy200 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_345 (f : SemanticCore.Var) : nb057AlphaDummy201 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_346 : nb057AlphaDummy236 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_347 (f : SemanticCore.Var) : nb057AlphaDummy237 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_348 : nb057AlphaDummy276 ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy243)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_349 (f : SemanticCore.Var) : nb057AlphaDummy277 f ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy245 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_350 : nb057AlphaDummy002 ∉ {nb057AlphaDummy001} ∪ {nb057AlphaDummy000} ∪ (Compiler.CompactSourceSyntax.synWfn (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy000)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_351 : nb057AlphaDummy050 ∉ {nb057AlphaDummy044} ∪ {nb057AlphaDummy045} ∪ (Compiler.CompactSourceSyntax.synWex nb057AlphaDummy046 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy044) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001)) (SemanticCore.Class.cv nb057AlphaDummy046)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy045)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_352 (f : SemanticCore.Var) : nb057AlphaDummy051 f ∉ {nb057AlphaDummy047 f} ∪ {nb057AlphaDummy048 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb057AlphaDummy049 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb057AlphaDummy049 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb057AlphaDummy048 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_353 : nb057AlphaDummy128 ∉ {nb057AlphaDummy124} ∪ {nb057AlphaDummy125} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy124)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_354 (f : SemanticCore.Var) : nb057AlphaDummy129 f ∉ {nb057AlphaDummy126 f} ∪ {nb057AlphaDummy127 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb057AlphaDummy126 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_355 (f a : SemanticCore.Var) : nb057AlphaDummy003 f a ∉ {f} ∪ {a} ∪ (Compiler.CompactSourceSyntax.synWfn (SemanticCore.Class.cv f) (SemanticCore.Class.cv a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_356 : nb057AlphaDummy000 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_fresh_357 : nb057AlphaDummy001 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_distinct_358 : nb057AlphaDummy000 ≠ nb057AlphaDummy001

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0000 : nb057AlphaDummy001 ∈ {nb057AlphaDummy001} ∪ {nb057AlphaDummy000} ∪ (Compiler.CompactSourceSyntax.synWfn (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy000)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0001 (f a : SemanticCore.Var) : f ∈ {f} ∪ {a} ∪ (Compiler.CompactSourceSyntax.synWfn (SemanticCore.Class.cv f) (SemanticCore.Class.cv a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0002 : nb057AlphaDummy000 ∈ {nb057AlphaDummy001} ∪ {nb057AlphaDummy000} ∪ (Compiler.CompactSourceSyntax.synWfn (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy000)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0003 (f a : SemanticCore.Var) : a ∈ {f} ∪ {a} ∪ (Compiler.CompactSourceSyntax.synWfn (SemanticCore.Class.cv f) (SemanticCore.Class.cv a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0004 : nb057AlphaDummy001 ∈ (SemanticCore.Class.cv nb057AlphaDummy001).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy000).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0005 : nb057AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy004 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy005 (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy004) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy004 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy005 (SemanticCore.Class.cv nb057AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy004) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0006 (f a : SemanticCore.Var) : f ∈ (SemanticCore.Class.cv f).fv ∪ (SemanticCore.Class.cv a).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0007 (f a : SemanticCore.Var) : f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy006 f a) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy007 f a) (SemanticCore.Class.cv f) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy006 f a)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy006 f a) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy007 f a) (SemanticCore.Class.cv a) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy006 f a)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0008 : nb057AlphaDummy001 ∈ (SemanticCore.Class.cab nb057AlphaDummy004 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy005 (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy004) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy004 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy005 (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy004) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0009 (f a : SemanticCore.Var) : f ∈ (SemanticCore.Class.cab (nb057AlphaDummy006 f a) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy007 f a) (SemanticCore.Class.cv f) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy006 f a)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a)))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy006 f a) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy007 f a) (SemanticCore.Class.cv f) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy006 f a)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0010 : nb057AlphaDummy005 ∈ (SemanticCore.Class.cv nb057AlphaDummy005).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0011 (f a : SemanticCore.Var) : nb057AlphaDummy007 f a ∈ (SemanticCore.Class.cv (nb057AlphaDummy007 f a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0012 : nb057AlphaDummy012 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy012) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy012) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy012).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0013 (f a : SemanticCore.Var) : nb057AlphaDummy014 f a ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy014 f a)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy014 f a)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy014 f a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0014 : nb057AlphaDummy012 ∈ (SemanticCore.Class.cv nb057AlphaDummy012).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0015 (f a : SemanticCore.Var) : nb057AlphaDummy014 f a ∈ (SemanticCore.Class.cv (nb057AlphaDummy014 f a)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0016 : nb057AlphaDummy019 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy019) (SemanticCore.Class.cv nb057AlphaDummy020)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy019) (SemanticCore.Class.cv nb057AlphaDummy020)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0017 (f a : SemanticCore.Var) : nb057AlphaDummy022 f a ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy022 f a)) (SemanticCore.Class.cv (nb057AlphaDummy023 f a))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy022 f a)) (SemanticCore.Class.cv (nb057AlphaDummy023 f a))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0018 : nb057AlphaDummy019 ∈ (SemanticCore.Class.cv nb057AlphaDummy019).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy020).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0019 (f a : SemanticCore.Var) : nb057AlphaDummy022 f a ∈ (SemanticCore.Class.cv (nb057AlphaDummy022 f a)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy023 f a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0020 : nb057AlphaDummy020 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy019) (SemanticCore.Class.cv nb057AlphaDummy020)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy019) (SemanticCore.Class.cv nb057AlphaDummy020)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0021 (f a : SemanticCore.Var) : nb057AlphaDummy023 f a ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy022 f a)) (SemanticCore.Class.cv (nb057AlphaDummy023 f a))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy022 f a)) (SemanticCore.Class.cv (nb057AlphaDummy023 f a))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0022 : nb057AlphaDummy020 ∈ (SemanticCore.Class.cv nb057AlphaDummy019).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy020).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0023 (f a : SemanticCore.Var) : nb057AlphaDummy023 f a ∈ (SemanticCore.Class.cv (nb057AlphaDummy022 f a)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy023 f a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0024 : nb057AlphaDummy019 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy019)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy020)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0025 (f a : SemanticCore.Var) : nb057AlphaDummy022 f a ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy022 f a))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy023 f a))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0026 : nb057AlphaDummy019 ∈ (SemanticCore.Class.cv nb057AlphaDummy019).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy019).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0027 (f a : SemanticCore.Var) : nb057AlphaDummy022 f a ∈ (SemanticCore.Class.cv (nb057AlphaDummy022 f a)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy022 f a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0028 : nb057AlphaDummy020 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy019)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy020)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0029 (f a : SemanticCore.Var) : nb057AlphaDummy023 f a ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy022 f a))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy023 f a))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0030 : nb057AlphaDummy020 ∈ (SemanticCore.Class.cv nb057AlphaDummy020).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy020).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0031 (f a : SemanticCore.Var) : nb057AlphaDummy023 f a ∈ (SemanticCore.Class.cv (nb057AlphaDummy023 f a)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy023 f a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0032 : nb057AlphaDummy000 ∈ (SemanticCore.Class.cv nb057AlphaDummy001).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy000).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0033 : nb057AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy004 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy005 (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy004) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy004 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy005 (SemanticCore.Class.cv nb057AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy004) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0034 (f a : SemanticCore.Var) : a ∈ (SemanticCore.Class.cv f).fv ∪ (SemanticCore.Class.cv a).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0035 (f a : SemanticCore.Var) : a ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy006 f a) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy007 f a) (SemanticCore.Class.cv f) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy006 f a)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy006 f a) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy007 f a) (SemanticCore.Class.cv a) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy006 f a)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0036 : nb057AlphaDummy000 ∈ (SemanticCore.Class.cab nb057AlphaDummy004 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy005 (SemanticCore.Class.cv nb057AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy004) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy004 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy005 (SemanticCore.Class.cv nb057AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy004) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0037 (f a : SemanticCore.Var) : a ∈ (SemanticCore.Class.cab (nb057AlphaDummy006 f a) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy007 f a) (SemanticCore.Class.cv a) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy006 f a)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy006 f a) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy007 f a) (SemanticCore.Class.cv a) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy006 f a)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0038 : nb057AlphaDummy005 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0039 (f a : SemanticCore.Var) : nb057AlphaDummy007 f a ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0040 : nb057AlphaDummy005 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy005)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0041 (f a : SemanticCore.Var) : nb057AlphaDummy007 f a ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy007 f a))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0042 : nb057AlphaDummy044 ∈ {nb057AlphaDummy044} ∪ {nb057AlphaDummy045} ∪ (Compiler.CompactSourceSyntax.synWex nb057AlphaDummy046 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy044) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001)) (SemanticCore.Class.cv nb057AlphaDummy046)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy045)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0043 (f : SemanticCore.Var) : nb057AlphaDummy047 f ∈ {nb057AlphaDummy047 f} ∪ {nb057AlphaDummy048 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb057AlphaDummy049 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb057AlphaDummy049 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb057AlphaDummy048 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0044 : nb057AlphaDummy045 ∈ {nb057AlphaDummy044} ∪ {nb057AlphaDummy045} ∪ (Compiler.CompactSourceSyntax.synWex nb057AlphaDummy046 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy044) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001)) (SemanticCore.Class.cv nb057AlphaDummy046)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy045)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0045 (f : SemanticCore.Var) : nb057AlphaDummy048 f ∈ {nb057AlphaDummy047 f} ∪ {nb057AlphaDummy048 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb057AlphaDummy049 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb057AlphaDummy049 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb057AlphaDummy048 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0046 : nb057AlphaDummy044 ∈ (SemanticCore.Class.cv nb057AlphaDummy044).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy045).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0047 : nb057AlphaDummy044 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy052 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy053 (SemanticCore.Class.cv nb057AlphaDummy044) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy052) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy052 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy053 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy052) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0048 (f : SemanticCore.Var) : nb057AlphaDummy047 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy047 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy048 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0049 (f : SemanticCore.Var) : nb057AlphaDummy047 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy054 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy055 f) (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy054 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy054 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy055 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy054 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0050 : nb057AlphaDummy044 ∈ (SemanticCore.Class.cab nb057AlphaDummy052 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy053 (SemanticCore.Class.cv nb057AlphaDummy044) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy052) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy052 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy053 (SemanticCore.Class.cv nb057AlphaDummy044) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy052) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0051 (f : SemanticCore.Var) : nb057AlphaDummy047 f ∈ (SemanticCore.Class.cab (nb057AlphaDummy054 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy055 f) (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy054 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f)))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy054 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy055 f) (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy054 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0052 : nb057AlphaDummy053 ∈ (SemanticCore.Class.cv nb057AlphaDummy053).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0053 (f : SemanticCore.Var) : nb057AlphaDummy055 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy055 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0054 : nb057AlphaDummy060 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy060) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy060) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy060).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0055 (f : SemanticCore.Var) : nb057AlphaDummy062 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy062 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy062 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy062 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0056 : nb057AlphaDummy060 ∈ (SemanticCore.Class.cv nb057AlphaDummy060).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0057 (f : SemanticCore.Var) : nb057AlphaDummy062 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy062 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0058 : nb057AlphaDummy067 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy067) (SemanticCore.Class.cv nb057AlphaDummy068)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy067) (SemanticCore.Class.cv nb057AlphaDummy068)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0059 (f : SemanticCore.Var) : nb057AlphaDummy070 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy070 f)) (SemanticCore.Class.cv (nb057AlphaDummy071 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy070 f)) (SemanticCore.Class.cv (nb057AlphaDummy071 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0060 : nb057AlphaDummy067 ∈ (SemanticCore.Class.cv nb057AlphaDummy067).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy068).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0061 (f : SemanticCore.Var) : nb057AlphaDummy070 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy070 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy071 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0062 : nb057AlphaDummy068 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy067) (SemanticCore.Class.cv nb057AlphaDummy068)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy067) (SemanticCore.Class.cv nb057AlphaDummy068)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0063 (f : SemanticCore.Var) : nb057AlphaDummy071 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy070 f)) (SemanticCore.Class.cv (nb057AlphaDummy071 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy070 f)) (SemanticCore.Class.cv (nb057AlphaDummy071 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0064 : nb057AlphaDummy068 ∈ (SemanticCore.Class.cv nb057AlphaDummy067).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy068).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0065 (f : SemanticCore.Var) : nb057AlphaDummy071 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy070 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy071 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0066 : nb057AlphaDummy067 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy067)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy068)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0067 (f : SemanticCore.Var) : nb057AlphaDummy070 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy070 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy071 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0068 : nb057AlphaDummy067 ∈ (SemanticCore.Class.cv nb057AlphaDummy067).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy067).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0069 (f : SemanticCore.Var) : nb057AlphaDummy070 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy070 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy070 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0070 : nb057AlphaDummy068 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy067)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy068)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0071 (f : SemanticCore.Var) : nb057AlphaDummy071 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy070 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy071 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0072 : nb057AlphaDummy068 ∈ (SemanticCore.Class.cv nb057AlphaDummy068).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy068).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0073 (f : SemanticCore.Var) : nb057AlphaDummy071 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy071 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy071 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0074 : nb057AlphaDummy045 ∈ (SemanticCore.Class.cv nb057AlphaDummy044).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy045).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0075 : nb057AlphaDummy045 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy052 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy053 (SemanticCore.Class.cv nb057AlphaDummy044) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy052) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy052 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy053 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy052) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0076 (f : SemanticCore.Var) : nb057AlphaDummy048 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy047 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy048 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0077 (f : SemanticCore.Var) : nb057AlphaDummy048 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy054 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy055 f) (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy054 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy054 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy055 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy054 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0078 : nb057AlphaDummy045 ∈ (SemanticCore.Class.cab nb057AlphaDummy052 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy053 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy052) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy052 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy053 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy052) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0079 (f : SemanticCore.Var) : nb057AlphaDummy048 f ∈ (SemanticCore.Class.cab (nb057AlphaDummy054 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy055 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy054 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy054 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy055 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy054 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0080 : nb057AlphaDummy053 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0081 (f : SemanticCore.Var) : nb057AlphaDummy055 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0082 : nb057AlphaDummy053 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy053)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0083 (f : SemanticCore.Var) : nb057AlphaDummy055 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy055 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0084 : nb057AlphaDummy044 ∈ (SemanticCore.Class.cv nb057AlphaDummy044).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy046).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0085 : nb057AlphaDummy044 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy088 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy089 (SemanticCore.Class.cv nb057AlphaDummy044) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy088) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy088 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy089 (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy088) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0086 (f : SemanticCore.Var) : nb057AlphaDummy047 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy047 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy049 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0087 (f : SemanticCore.Var) : nb057AlphaDummy047 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy090 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy091 f) (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy090 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy091 f) (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0088 : nb057AlphaDummy044 ∈ (SemanticCore.Class.cab nb057AlphaDummy088 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy089 (SemanticCore.Class.cv nb057AlphaDummy044) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy088) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy088 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy089 (SemanticCore.Class.cv nb057AlphaDummy044) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy088) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0089 (f : SemanticCore.Var) : nb057AlphaDummy047 f ∈ (SemanticCore.Class.cab (nb057AlphaDummy090 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy091 f) (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f)))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy090 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy091 f) (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0090 : nb057AlphaDummy089 ∈ (SemanticCore.Class.cv nb057AlphaDummy089).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0091 (f : SemanticCore.Var) : nb057AlphaDummy091 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy091 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0092 : nb057AlphaDummy096 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy096) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy096) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy096).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0093 (f : SemanticCore.Var) : nb057AlphaDummy098 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy098 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy098 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy098 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0094 : nb057AlphaDummy096 ∈ (SemanticCore.Class.cv nb057AlphaDummy096).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0095 (f : SemanticCore.Var) : nb057AlphaDummy098 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy098 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0096 : nb057AlphaDummy103 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy103) (SemanticCore.Class.cv nb057AlphaDummy104)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy103) (SemanticCore.Class.cv nb057AlphaDummy104)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0097 (f : SemanticCore.Var) : nb057AlphaDummy106 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy106 f)) (SemanticCore.Class.cv (nb057AlphaDummy107 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy106 f)) (SemanticCore.Class.cv (nb057AlphaDummy107 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0098 : nb057AlphaDummy103 ∈ (SemanticCore.Class.cv nb057AlphaDummy103).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy104).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0099 (f : SemanticCore.Var) : nb057AlphaDummy106 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy106 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy107 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0100 : nb057AlphaDummy104 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy103) (SemanticCore.Class.cv nb057AlphaDummy104)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy103) (SemanticCore.Class.cv nb057AlphaDummy104)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0101 (f : SemanticCore.Var) : nb057AlphaDummy107 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy106 f)) (SemanticCore.Class.cv (nb057AlphaDummy107 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy106 f)) (SemanticCore.Class.cv (nb057AlphaDummy107 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0102 : nb057AlphaDummy104 ∈ (SemanticCore.Class.cv nb057AlphaDummy103).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy104).fv

Certificates from NAR4C057C001Part006.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0103 (f : SemanticCore.Var) : nb057AlphaDummy107 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy106 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy107 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0104 : nb057AlphaDummy103 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy103)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy104)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0105 (f : SemanticCore.Var) : nb057AlphaDummy106 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy106 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy107 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0106 : nb057AlphaDummy103 ∈ (SemanticCore.Class.cv nb057AlphaDummy103).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy103).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0107 (f : SemanticCore.Var) : nb057AlphaDummy106 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy106 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy106 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0108 : nb057AlphaDummy104 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy103)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy104)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0109 (f : SemanticCore.Var) : nb057AlphaDummy107 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy106 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy107 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0110 : nb057AlphaDummy104 ∈ (SemanticCore.Class.cv nb057AlphaDummy104).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy104).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0111 (f : SemanticCore.Var) : nb057AlphaDummy107 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy107 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy107 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0112 : nb057AlphaDummy046 ∈ (SemanticCore.Class.cv nb057AlphaDummy044).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy046).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0113 : nb057AlphaDummy046 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy088 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy089 (SemanticCore.Class.cv nb057AlphaDummy044) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy088) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy088 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy089 (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy088) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0114 (f : SemanticCore.Var) : nb057AlphaDummy049 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy047 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy049 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0115 (f : SemanticCore.Var) : nb057AlphaDummy049 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy090 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy091 f) (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy090 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy091 f) (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0116 : nb057AlphaDummy046 ∈ (SemanticCore.Class.cab nb057AlphaDummy088 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy089 (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy088) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy088 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy089 (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy088) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0117 (f : SemanticCore.Var) : nb057AlphaDummy049 f ∈ (SemanticCore.Class.cab (nb057AlphaDummy090 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy091 f) (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy090 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy091 f) (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0118 : nb057AlphaDummy089 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0119 (f : SemanticCore.Var) : nb057AlphaDummy091 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0120 : nb057AlphaDummy089 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy089)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0121 (f : SemanticCore.Var) : nb057AlphaDummy091 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy091 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0122 : nb057AlphaDummy124 ∈ {nb057AlphaDummy124} ∪ {nb057AlphaDummy125} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy124)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0123 (f : SemanticCore.Var) : nb057AlphaDummy126 f ∈ {nb057AlphaDummy126 f} ∪ {nb057AlphaDummy127 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb057AlphaDummy126 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0124 : nb057AlphaDummy125 ∈ {nb057AlphaDummy124} ∪ {nb057AlphaDummy125} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy124)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0125 (f : SemanticCore.Var) : nb057AlphaDummy127 f ∈ {nb057AlphaDummy126 f} ∪ {nb057AlphaDummy127 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb057AlphaDummy126 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0126 : nb057AlphaDummy124 ∈ (SemanticCore.Class.cv nb057AlphaDummy124).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy125).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0127 : nb057AlphaDummy124 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0128 (f : SemanticCore.Var) : nb057AlphaDummy126 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy126 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy127 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0129 (f : SemanticCore.Var) : nb057AlphaDummy126 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0130 : nb057AlphaDummy124 ∈ (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0131 (f : SemanticCore.Var) : nb057AlphaDummy126 f ∈ (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f)))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0132 : nb057AlphaDummy131 ∈ (SemanticCore.Class.cv nb057AlphaDummy131).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0133 (f : SemanticCore.Var) : nb057AlphaDummy133 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy133 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0134 : nb057AlphaDummy138 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy138) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy138) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy138).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0135 (f : SemanticCore.Var) : nb057AlphaDummy140 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy140 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy140 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy140 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0136 : nb057AlphaDummy138 ∈ (SemanticCore.Class.cv nb057AlphaDummy138).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0137 (f : SemanticCore.Var) : nb057AlphaDummy140 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy140 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0138 : nb057AlphaDummy145 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0139 (f : SemanticCore.Var) : nb057AlphaDummy148 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0140 : nb057AlphaDummy145 ∈ (SemanticCore.Class.cv nb057AlphaDummy145).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy146).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0141 (f : SemanticCore.Var) : nb057AlphaDummy148 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy148 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy149 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0142 : nb057AlphaDummy146 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy145) (SemanticCore.Class.cv nb057AlphaDummy146)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0143 (f : SemanticCore.Var) : nb057AlphaDummy149 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy148 f)) (SemanticCore.Class.cv (nb057AlphaDummy149 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0144 : nb057AlphaDummy146 ∈ (SemanticCore.Class.cv nb057AlphaDummy145).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy146).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0145 (f : SemanticCore.Var) : nb057AlphaDummy149 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy148 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy149 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0146 : nb057AlphaDummy145 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy145)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy146)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0147 (f : SemanticCore.Var) : nb057AlphaDummy148 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy148 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy149 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0148 : nb057AlphaDummy145 ∈ (SemanticCore.Class.cv nb057AlphaDummy145).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy145).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0149 (f : SemanticCore.Var) : nb057AlphaDummy148 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy148 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy148 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0150 : nb057AlphaDummy146 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy145)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy146)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0151 (f : SemanticCore.Var) : nb057AlphaDummy149 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy148 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy149 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0152 : nb057AlphaDummy146 ∈ (SemanticCore.Class.cv nb057AlphaDummy146).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy146).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0153 (f : SemanticCore.Var) : nb057AlphaDummy149 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy149 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy149 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0154 : nb057AlphaDummy125 ∈ (SemanticCore.Class.cv nb057AlphaDummy124).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy125).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0155 : nb057AlphaDummy125 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0156 (f : SemanticCore.Var) : nb057AlphaDummy127 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy126 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy127 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0157 (f : SemanticCore.Var) : nb057AlphaDummy127 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0158 : nb057AlphaDummy125 ∈ (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy130 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy131 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy130) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0159 (f : SemanticCore.Var) : nb057AlphaDummy127 f ∈ (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy132 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy133 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy132 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0160 : nb057AlphaDummy131 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0161 (f : SemanticCore.Var) : nb057AlphaDummy133 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0162 : nb057AlphaDummy131 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy131)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0163 (f : SemanticCore.Var) : nb057AlphaDummy133 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy133 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0164 : nb057AlphaDummy125 ∈ (SemanticCore.Class.cv nb057AlphaDummy125).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy124).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0165 : nb057AlphaDummy125 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0166 (f : SemanticCore.Var) : nb057AlphaDummy127 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy127 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy126 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0167 (f : SemanticCore.Var) : nb057AlphaDummy127 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0168 : nb057AlphaDummy125 ∈ (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0169 (f : SemanticCore.Var) : nb057AlphaDummy127 f ∈ (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f)))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0170 : nb057AlphaDummy167 ∈ (SemanticCore.Class.cv nb057AlphaDummy167).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0171 (f : SemanticCore.Var) : nb057AlphaDummy169 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy169 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0172 : nb057AlphaDummy174 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy174) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy174) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy174).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0173 (f : SemanticCore.Var) : nb057AlphaDummy176 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy176 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy176 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy176 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0174 : nb057AlphaDummy174 ∈ (SemanticCore.Class.cv nb057AlphaDummy174).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0175 (f : SemanticCore.Var) : nb057AlphaDummy176 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy176 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0176 : nb057AlphaDummy181 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0177 (f : SemanticCore.Var) : nb057AlphaDummy184 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0178 : nb057AlphaDummy181 ∈ (SemanticCore.Class.cv nb057AlphaDummy181).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy182).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0179 (f : SemanticCore.Var) : nb057AlphaDummy184 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy184 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy185 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0180 : nb057AlphaDummy182 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy181) (SemanticCore.Class.cv nb057AlphaDummy182)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0181 (f : SemanticCore.Var) : nb057AlphaDummy185 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy184 f)) (SemanticCore.Class.cv (nb057AlphaDummy185 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0182 : nb057AlphaDummy182 ∈ (SemanticCore.Class.cv nb057AlphaDummy181).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy182).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0183 (f : SemanticCore.Var) : nb057AlphaDummy185 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy184 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy185 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0184 : nb057AlphaDummy181 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy181)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy182)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0185 (f : SemanticCore.Var) : nb057AlphaDummy184 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy184 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy185 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0186 : nb057AlphaDummy181 ∈ (SemanticCore.Class.cv nb057AlphaDummy181).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy181).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0187 (f : SemanticCore.Var) : nb057AlphaDummy184 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy184 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy184 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0188 : nb057AlphaDummy182 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy181)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy182)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0189 (f : SemanticCore.Var) : nb057AlphaDummy185 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy184 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy185 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0190 : nb057AlphaDummy182 ∈ (SemanticCore.Class.cv nb057AlphaDummy182).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy182).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0191 (f : SemanticCore.Var) : nb057AlphaDummy185 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy185 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy185 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0192 : nb057AlphaDummy124 ∈ (SemanticCore.Class.cv nb057AlphaDummy125).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy124).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0193 : nb057AlphaDummy124 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0194 (f : SemanticCore.Var) : nb057AlphaDummy126 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy127 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy126 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0195 (f : SemanticCore.Var) : nb057AlphaDummy126 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0196 : nb057AlphaDummy124 ∈ (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy166 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy167 (SemanticCore.Class.cv nb057AlphaDummy124) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy166) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0197 (f : SemanticCore.Var) : nb057AlphaDummy126 f ∈ (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy168 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy169 f) (SemanticCore.Class.cv (nb057AlphaDummy126 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0198 : nb057AlphaDummy167 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0199 (f : SemanticCore.Var) : nb057AlphaDummy169 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0200 : nb057AlphaDummy167 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy167)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0201 (f : SemanticCore.Var) : nb057AlphaDummy169 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy169 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0202 : nb057AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb057AlphaDummy001) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001))) Compiler.CompactSourceSyntax.synCid).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb057AlphaDummy001) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001))) Compiler.CompactSourceSyntax.synCid).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0204 : nb057AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb057AlphaDummy001) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001))).fv ∪ Compiler.CompactSourceSyntax.synCid.fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0206 : nb057AlphaDummy001 ∈ (SemanticCore.Class.cv nb057AlphaDummy001).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0207 : nb057AlphaDummy001 ∈ {nb057AlphaDummy044} ∪ {nb057AlphaDummy045} ∪ (Compiler.CompactSourceSyntax.synWex nb057AlphaDummy046 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy044) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb057AlphaDummy001)) (SemanticCore.Class.cv nb057AlphaDummy046)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy045)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0208 (f : SemanticCore.Var) : f ∈ (SemanticCore.Class.cv f).fv ∪ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0209 (f : SemanticCore.Var) : f ∈ {nb057AlphaDummy047 f} ∪ {nb057AlphaDummy048 f} ∪ (Compiler.CompactSourceSyntax.synWex (nb057AlphaDummy049 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy047 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb057AlphaDummy049 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb057AlphaDummy048 f))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0210 : nb057AlphaDummy001 ∈ {nb057AlphaDummy124} ∪ {nb057AlphaDummy125} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb057AlphaDummy125) (SemanticCore.Class.cv nb057AlphaDummy001) (SemanticCore.Class.cv nb057AlphaDummy124)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0211 (f : SemanticCore.Var) : f ∈ {nb057AlphaDummy126 f} ∪ {nb057AlphaDummy127 f} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb057AlphaDummy127 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb057AlphaDummy126 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0212 : nb057AlphaDummy001 ∈ (SemanticCore.Class.cv nb057AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0213 (f : SemanticCore.Var) : f ∈ (SemanticCore.Class.cv f).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0214 : nb057AlphaDummy046 ∈ (SemanticCore.Class.cv nb057AlphaDummy046).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy045).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0215 : nb057AlphaDummy046 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy202 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy203 (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy202) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy202 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy203 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy202) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0216 (f : SemanticCore.Var) : nb057AlphaDummy049 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy049 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy048 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0217 (f : SemanticCore.Var) : nb057AlphaDummy049 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy204 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy205 f) (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy204 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy204 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy205 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy204 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0218 : nb057AlphaDummy046 ∈ (SemanticCore.Class.cab nb057AlphaDummy202 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy203 (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy202) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203))))).fv ∪ (SemanticCore.Class.cab nb057AlphaDummy202 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy203 (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy202) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0219 (f : SemanticCore.Var) : nb057AlphaDummy049 f ∈ (SemanticCore.Class.cab (nb057AlphaDummy204 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy205 f) (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy204 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f)))))).fv ∪ (SemanticCore.Class.cab (nb057AlphaDummy204 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy205 f) (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy204 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0220 : nb057AlphaDummy203 ∈ (SemanticCore.Class.cv nb057AlphaDummy203).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0221 (f : SemanticCore.Var) : nb057AlphaDummy205 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy205 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0222 : nb057AlphaDummy210 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb057AlphaDummy210) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb057AlphaDummy210) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy210).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0223 (f : SemanticCore.Var) : nb057AlphaDummy212 f ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb057AlphaDummy212 f)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb057AlphaDummy212 f)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy212 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0224 : nb057AlphaDummy210 ∈ (SemanticCore.Class.cv nb057AlphaDummy210).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0225 (f : SemanticCore.Var) : nb057AlphaDummy212 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy212 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0226 : nb057AlphaDummy217 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy217) (SemanticCore.Class.cv nb057AlphaDummy218)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy217) (SemanticCore.Class.cv nb057AlphaDummy218)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0227 (f : SemanticCore.Var) : nb057AlphaDummy220 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy220 f)) (SemanticCore.Class.cv (nb057AlphaDummy221 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy220 f)) (SemanticCore.Class.cv (nb057AlphaDummy221 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0228 : nb057AlphaDummy217 ∈ (SemanticCore.Class.cv nb057AlphaDummy217).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy218).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0229 (f : SemanticCore.Var) : nb057AlphaDummy220 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy220 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy221 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0230 : nb057AlphaDummy218 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy217) (SemanticCore.Class.cv nb057AlphaDummy218)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb057AlphaDummy217) (SemanticCore.Class.cv nb057AlphaDummy218)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0231 (f : SemanticCore.Var) : nb057AlphaDummy221 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy220 f)) (SemanticCore.Class.cv (nb057AlphaDummy221 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb057AlphaDummy220 f)) (SemanticCore.Class.cv (nb057AlphaDummy221 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0232 : nb057AlphaDummy218 ∈ (SemanticCore.Class.cv nb057AlphaDummy217).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy218).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0233 (f : SemanticCore.Var) : nb057AlphaDummy221 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy220 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy221 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0234 : nb057AlphaDummy217 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy217)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy218)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0235 (f : SemanticCore.Var) : nb057AlphaDummy220 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy220 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy221 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0236 : nb057AlphaDummy217 ∈ (SemanticCore.Class.cv nb057AlphaDummy217).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy217).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0237 (f : SemanticCore.Var) : nb057AlphaDummy220 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy220 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy220 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0238 : nb057AlphaDummy218 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy217)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb057AlphaDummy218)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0239 (f : SemanticCore.Var) : nb057AlphaDummy221 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy220 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb057AlphaDummy221 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0240 : nb057AlphaDummy218 ∈ (SemanticCore.Class.cv nb057AlphaDummy218).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy218).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0241 (f : SemanticCore.Var) : nb057AlphaDummy221 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy221 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy221 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0242 : nb057AlphaDummy045 ∈ (SemanticCore.Class.cv nb057AlphaDummy046).fv ∪ (SemanticCore.Class.cv nb057AlphaDummy045).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0243 : nb057AlphaDummy045 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy202 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy203 (SemanticCore.Class.cv nb057AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy202) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb057AlphaDummy202 (Compiler.CompactSourceSyntax.synWrex nb057AlphaDummy203 (SemanticCore.Class.cv nb057AlphaDummy045) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb057AlphaDummy202) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb057AlphaDummy203)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0244 (f : SemanticCore.Var) : nb057AlphaDummy048 f ∈ (SemanticCore.Class.cv (nb057AlphaDummy049 f)).fv ∪ (SemanticCore.Class.cv (nb057AlphaDummy048 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb057_support_mem_0245 (f : SemanticCore.Var) : nb057AlphaDummy048 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy204 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy205 f) (SemanticCore.Class.cv (nb057AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy204 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb057AlphaDummy204 f) (Compiler.CompactSourceSyntax.synWrex (nb057AlphaDummy205 f) (SemanticCore.Class.cv (nb057AlphaDummy048 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb057AlphaDummy204 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb057AlphaDummy205 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv