Nominal proof certificates grouped in dependency order.

Certificates from NAR4C090C001Part020.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0635 (h : SemanticCore.Var) : nb090AlphaDummy427 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy583 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy584 h) (SemanticCore.Class.cv (nb090AlphaDummy428 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy583 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy583 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy584 h) (SemanticCore.Class.cv (nb090AlphaDummy427 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy583 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0636 (A : SemanticCore.Class) : nb090AlphaDummy424 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy581 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy582 A) (SemanticCore.Class.cv (nb090AlphaDummy424 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy581 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy581 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy582 A) (SemanticCore.Class.cv (nb090AlphaDummy424 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy581 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0637 (h : SemanticCore.Var) : nb090AlphaDummy427 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy583 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy584 h) (SemanticCore.Class.cv (nb090AlphaDummy427 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy583 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy583 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy584 h) (SemanticCore.Class.cv (nb090AlphaDummy427 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy583 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0639 (h : SemanticCore.Var) : nb090AlphaDummy584 h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0640 (A : SemanticCore.Class) : nb090AlphaDummy582 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0641 (h : SemanticCore.Var) : nb090AlphaDummy584 h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0642 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy000 A)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy001 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy002 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy001 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0643 (v u h : SemanticCore.Var) : u ∈ (SemanticCore.Class.cv h).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0644 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy041 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy042 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0645 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy617 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy618 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy617 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy617 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy618 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy617 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0646 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0647 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy619 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy620 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy619 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy619 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy620 v u h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy619 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0648 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy617 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy618 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy617 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy617 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy618 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy617 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0649 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ (SemanticCore.Class.cab (nb090AlphaDummy619 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy620 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy619 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy619 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy620 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy619 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0650 (A : SemanticCore.Class) : nb090AlphaDummy618 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy618 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0651 (v u h : SemanticCore.Var) : nb090AlphaDummy620 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy620 v u h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0653 (v u h : SemanticCore.Var) : nb090AlphaDummy627 v u h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy627 v u h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy627 v u h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy627 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0654 (A : SemanticCore.Class) : nb090AlphaDummy625 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy625 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0655 (v u h : SemanticCore.Var) : nb090AlphaDummy627 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy627 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0656 (A : SemanticCore.Class) : nb090AlphaDummy632 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy632 A)) (SemanticCore.Class.cv (nb090AlphaDummy633 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy632 A)) (SemanticCore.Class.cv (nb090AlphaDummy633 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0657 (v u h : SemanticCore.Var) : nb090AlphaDummy635 v u h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy636 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy636 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0658 (A : SemanticCore.Class) : nb090AlphaDummy632 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy632 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy633 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0659 (v u h : SemanticCore.Var) : nb090AlphaDummy635 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy636 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0660 (A : SemanticCore.Class) : nb090AlphaDummy633 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy632 A)) (SemanticCore.Class.cv (nb090AlphaDummy633 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy632 A)) (SemanticCore.Class.cv (nb090AlphaDummy633 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0661 (v u h : SemanticCore.Var) : nb090AlphaDummy636 v u h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy636 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy636 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0662 (A : SemanticCore.Class) : nb090AlphaDummy633 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy632 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy633 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0663 (v u h : SemanticCore.Var) : nb090AlphaDummy636 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy636 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0664 (A : SemanticCore.Class) : nb090AlphaDummy632 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy632 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy633 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0665 (v u h : SemanticCore.Var) : nb090AlphaDummy635 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy635 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy636 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0666 (A : SemanticCore.Class) : nb090AlphaDummy632 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy632 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy632 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0667 (v u h : SemanticCore.Var) : nb090AlphaDummy635 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0668 (A : SemanticCore.Class) : nb090AlphaDummy633 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy632 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy633 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0669 (v u h : SemanticCore.Var) : nb090AlphaDummy636 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy635 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy636 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0670 (A : SemanticCore.Class) : nb090AlphaDummy633 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy633 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy633 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0671 (v u h : SemanticCore.Var) : nb090AlphaDummy636 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy636 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy636 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0672 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy041 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy042 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0673 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy617 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy618 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy617 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy617 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy618 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy617 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0674 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0675 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy619 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy620 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy619 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy619 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy620 v u h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy619 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0676 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy617 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy618 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy617 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy617 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy618 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy617 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0677 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ (SemanticCore.Class.cab (nb090AlphaDummy619 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy620 v u h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy619 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy619 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy620 v u h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy619 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0679 (v u h : SemanticCore.Var) : nb090AlphaDummy620 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0680 (A : SemanticCore.Class) : nb090AlphaDummy618 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0681 (v u h : SemanticCore.Var) : nb090AlphaDummy620 v u h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0682 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ Compiler.CompactSourceSyntax.synC1st.fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy001 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0683 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ {nb090AlphaDummy653 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy001 A)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy653 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0684 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy655 A) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy653 A) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy001 A)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy653 A)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy655 A))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0685 (u : SemanticCore.Var) : u ∈ Compiler.CompactSourceSyntax.synC1st.fv ∪ (SemanticCore.Class.cv u).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0686 (u : SemanticCore.Var) : u ∈ {nb090AlphaDummy654 u} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy654 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0687 (u : SemanticCore.Var) : u ∈ (SemanticCore.Class.cab (nb090AlphaDummy656 u) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy654 u) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy654 u)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy656 u))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0688 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy001 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy653 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0689 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy661 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy662 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy661 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy661 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy662 A) (SemanticCore.Class.cv (nb090AlphaDummy653 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy661 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0690 (u : SemanticCore.Var) : u ∈ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy654 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0691 (u : SemanticCore.Var) : u ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy663 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy664 u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy663 u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy663 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy664 u) (SemanticCore.Class.cv (nb090AlphaDummy654 u)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy663 u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0692 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy661 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy662 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy661 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy661 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy662 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy661 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0693 (u : SemanticCore.Var) : u ∈ (SemanticCore.Class.cab (nb090AlphaDummy663 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy664 u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy663 u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy663 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy664 u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy663 u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0694 (A : SemanticCore.Class) : nb090AlphaDummy662 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy662 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0695 (u : SemanticCore.Var) : nb090AlphaDummy664 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy664 u)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0697 (u : SemanticCore.Var) : nb090AlphaDummy671 u ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy671 u)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy671 u)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy671 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0698 (A : SemanticCore.Class) : nb090AlphaDummy669 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy669 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0699 (u : SemanticCore.Var) : nb090AlphaDummy671 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy671 u)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0700 (A : SemanticCore.Class) : nb090AlphaDummy676 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy676 A)) (SemanticCore.Class.cv (nb090AlphaDummy677 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy676 A)) (SemanticCore.Class.cv (nb090AlphaDummy677 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0701 (u : SemanticCore.Var) : nb090AlphaDummy679 u ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy679 u)) (SemanticCore.Class.cv (nb090AlphaDummy680 u))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy679 u)) (SemanticCore.Class.cv (nb090AlphaDummy680 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0702 (A : SemanticCore.Class) : nb090AlphaDummy676 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy676 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy677 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0703 (u : SemanticCore.Var) : nb090AlphaDummy679 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy679 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy680 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0704 (A : SemanticCore.Class) : nb090AlphaDummy677 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy676 A)) (SemanticCore.Class.cv (nb090AlphaDummy677 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy676 A)) (SemanticCore.Class.cv (nb090AlphaDummy677 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0705 (u : SemanticCore.Var) : nb090AlphaDummy680 u ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy679 u)) (SemanticCore.Class.cv (nb090AlphaDummy680 u))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy679 u)) (SemanticCore.Class.cv (nb090AlphaDummy680 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0706 (A : SemanticCore.Class) : nb090AlphaDummy677 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy676 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy677 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0707 (u : SemanticCore.Var) : nb090AlphaDummy680 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy679 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy680 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0708 (A : SemanticCore.Class) : nb090AlphaDummy676 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy676 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy677 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0709 (u : SemanticCore.Var) : nb090AlphaDummy679 u ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy679 u))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy680 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0710 (A : SemanticCore.Class) : nb090AlphaDummy676 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy676 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy676 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0711 (u : SemanticCore.Var) : nb090AlphaDummy679 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy679 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy679 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0712 (A : SemanticCore.Class) : nb090AlphaDummy677 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy676 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy677 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0713 (u : SemanticCore.Var) : nb090AlphaDummy680 u ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy679 u))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy680 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0714 (A : SemanticCore.Class) : nb090AlphaDummy677 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy677 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy677 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0715 (u : SemanticCore.Var) : nb090AlphaDummy680 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy680 u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy680 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0716 (A : SemanticCore.Class) : nb090AlphaDummy653 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy001 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy653 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0717 (A : SemanticCore.Class) : nb090AlphaDummy653 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy661 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy662 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy661 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy661 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy662 A) (SemanticCore.Class.cv (nb090AlphaDummy653 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy661 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0718 (u : SemanticCore.Var) : nb090AlphaDummy654 u ∈ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy654 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0719 (u : SemanticCore.Var) : nb090AlphaDummy654 u ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy663 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy664 u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy663 u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy663 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy664 u) (SemanticCore.Class.cv (nb090AlphaDummy654 u)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy663 u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0720 (A : SemanticCore.Class) : nb090AlphaDummy653 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy661 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy662 A) (SemanticCore.Class.cv (nb090AlphaDummy653 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy661 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy661 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy662 A) (SemanticCore.Class.cv (nb090AlphaDummy653 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy661 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0721 (u : SemanticCore.Var) : nb090AlphaDummy654 u ∈ (SemanticCore.Class.cab (nb090AlphaDummy663 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy664 u) (SemanticCore.Class.cv (nb090AlphaDummy654 u)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy663 u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy663 u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy664 u) (SemanticCore.Class.cv (nb090AlphaDummy654 u)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy663 u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0723 (u : SemanticCore.Var) : nb090AlphaDummy664 u ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0724 (A : SemanticCore.Class) : nb090AlphaDummy662 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0725 (u : SemanticCore.Var) : nb090AlphaDummy664 u ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0726 (A : SemanticCore.Class) : nb090AlphaDummy655 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy655 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0727 (u : SemanticCore.Var) : nb090AlphaDummy656 u ∈ (SemanticCore.Class.cv (nb090AlphaDummy656 u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0728 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0729 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0730 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0731 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0732 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0733 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0734 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy000 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy041 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0735 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ {nb090AlphaDummy707 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy707 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0736 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy709 A) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy707 A) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy707 A)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy709 A))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0737 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ (SemanticCore.Class.cv h).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0738 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ {nb090AlphaDummy708 v u h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy708 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0739 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ (SemanticCore.Class.cab (nb090AlphaDummy710 v u h) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy708 v u h) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy708 v u h)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy710 v u h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0740 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy041 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy707 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0741 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy707 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0742 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy708 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0743 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy708 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0744 (A : SemanticCore.Class) : nb090AlphaDummy041 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0745 (v u h : SemanticCore.Var) : nb090AlphaDummy043 v u h ∈ (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0746 (A : SemanticCore.Class) : nb090AlphaDummy716 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy716 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0747 (v u h : SemanticCore.Var) : nb090AlphaDummy718 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy718 v u h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0749 (v u h : SemanticCore.Var) : nb090AlphaDummy725 v u h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy725 v u h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy725 v u h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy725 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0750 (A : SemanticCore.Class) : nb090AlphaDummy723 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy723 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0751 (v u h : SemanticCore.Var) : nb090AlphaDummy725 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy725 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0752 (A : SemanticCore.Class) : nb090AlphaDummy730 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy730 A)) (SemanticCore.Class.cv (nb090AlphaDummy731 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy730 A)) (SemanticCore.Class.cv (nb090AlphaDummy731 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0753 (v u h : SemanticCore.Var) : nb090AlphaDummy733 v u h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy734 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy734 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0754 (A : SemanticCore.Class) : nb090AlphaDummy730 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy730 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy731 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0755 (v u h : SemanticCore.Var) : nb090AlphaDummy733 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy734 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0756 (A : SemanticCore.Class) : nb090AlphaDummy731 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy730 A)) (SemanticCore.Class.cv (nb090AlphaDummy731 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy730 A)) (SemanticCore.Class.cv (nb090AlphaDummy731 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0757 (v u h : SemanticCore.Var) : nb090AlphaDummy734 v u h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy734 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy734 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0758 (A : SemanticCore.Class) : nb090AlphaDummy731 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy730 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy731 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0759 (v u h : SemanticCore.Var) : nb090AlphaDummy734 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy734 v u h)).fv

Certificates from NAR4C090C001Part021.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0760 (A : SemanticCore.Class) : nb090AlphaDummy730 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy730 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy731 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0761 (v u h : SemanticCore.Var) : nb090AlphaDummy733 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy733 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy734 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0762 (A : SemanticCore.Class) : nb090AlphaDummy730 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy730 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy730 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0763 (v u h : SemanticCore.Var) : nb090AlphaDummy733 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0764 (A : SemanticCore.Class) : nb090AlphaDummy731 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy730 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy731 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0765 (v u h : SemanticCore.Var) : nb090AlphaDummy734 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy733 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy734 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0766 (A : SemanticCore.Class) : nb090AlphaDummy731 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy731 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy731 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0767 (v u h : SemanticCore.Var) : nb090AlphaDummy734 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy734 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy734 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0768 (A : SemanticCore.Class) : nb090AlphaDummy707 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy041 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy707 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0769 (A : SemanticCore.Class) : nb090AlphaDummy707 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy707 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0770 (v u h : SemanticCore.Var) : nb090AlphaDummy708 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy708 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0771 (v u h : SemanticCore.Var) : nb090AlphaDummy708 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy708 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0772 (A : SemanticCore.Class) : nb090AlphaDummy707 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy707 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy715 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy716 A) (SemanticCore.Class.cv (nb090AlphaDummy707 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy715 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0773 (v u h : SemanticCore.Var) : nb090AlphaDummy708 v u h ∈ (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy708 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy717 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy718 v u h) (SemanticCore.Class.cv (nb090AlphaDummy708 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy717 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0775 (v u h : SemanticCore.Var) : nb090AlphaDummy718 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0776 (A : SemanticCore.Class) : nb090AlphaDummy716 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0777 (v u h : SemanticCore.Var) : nb090AlphaDummy718 v u h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0778 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy000 A)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy001 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy002 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy001 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0779 (v u h : SemanticCore.Var) : h ∈ (SemanticCore.Class.cv h).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0780 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0781 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0782 (v u h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0783 (v u h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0784 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0785 (v u h : SemanticCore.Var) : h ∈ (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0786 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy000 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy041 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0787 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ {nb090AlphaDummy707 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy707 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0788 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy709 A) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy707 A) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy707 A)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy709 A))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0789 (v u h : SemanticCore.Var) : h ∈ (SemanticCore.Class.cv h).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0790 (v u h : SemanticCore.Var) : h ∈ {nb090AlphaDummy708 v u h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy708 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0791 (v u h : SemanticCore.Var) : h ∈ (SemanticCore.Class.cab (nb090AlphaDummy710 v u h) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy708 v u h) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy708 v u h)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy710 v u h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0792 (A : SemanticCore.Class) : nb090AlphaDummy709 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy709 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0793 (v u h : SemanticCore.Var) : nb090AlphaDummy710 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy710 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0794 (A : SemanticCore.Class) : nb090AlphaDummy700 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy700 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0795 (v u h : SemanticCore.Var) : nb090AlphaDummy702 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy702 v u h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0797 (v u h : SemanticCore.Var) : nb090AlphaDummy755 v u h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy755 v u h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy755 v u h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy755 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0798 (A : SemanticCore.Class) : nb090AlphaDummy753 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy753 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0799 (v u h : SemanticCore.Var) : nb090AlphaDummy755 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy755 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0800 (A : SemanticCore.Class) : nb090AlphaDummy760 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy760 A)) (SemanticCore.Class.cv (nb090AlphaDummy761 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy760 A)) (SemanticCore.Class.cv (nb090AlphaDummy761 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0801 (v u h : SemanticCore.Var) : nb090AlphaDummy763 v u h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy764 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy764 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0802 (A : SemanticCore.Class) : nb090AlphaDummy760 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy760 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy761 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0803 (v u h : SemanticCore.Var) : nb090AlphaDummy763 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy764 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0804 (A : SemanticCore.Class) : nb090AlphaDummy761 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy760 A)) (SemanticCore.Class.cv (nb090AlphaDummy761 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy760 A)) (SemanticCore.Class.cv (nb090AlphaDummy761 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0805 (v u h : SemanticCore.Var) : nb090AlphaDummy764 v u h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy764 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy764 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0806 (A : SemanticCore.Class) : nb090AlphaDummy761 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy760 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy761 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0807 (v u h : SemanticCore.Var) : nb090AlphaDummy764 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy764 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0808 (A : SemanticCore.Class) : nb090AlphaDummy760 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy760 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy761 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0809 (v u h : SemanticCore.Var) : nb090AlphaDummy763 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy763 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy764 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0810 (A : SemanticCore.Class) : nb090AlphaDummy760 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy760 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy760 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0811 (v u h : SemanticCore.Var) : nb090AlphaDummy763 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0812 (A : SemanticCore.Class) : nb090AlphaDummy761 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy760 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy761 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0813 (v u h : SemanticCore.Var) : nb090AlphaDummy764 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy763 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy764 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0814 (A : SemanticCore.Class) : nb090AlphaDummy761 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy761 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy761 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0815 (v u h : SemanticCore.Var) : nb090AlphaDummy764 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy764 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy764 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0816 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0817 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0818 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0819 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0820 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0821 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0822 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy000 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy042 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0823 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ {nb090AlphaDummy777 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy777 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0824 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy779 A) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy777 A) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy777 A)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy779 A))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0825 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ (SemanticCore.Class.cv h).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0826 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ {nb090AlphaDummy778 v u h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy778 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0827 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ (SemanticCore.Class.cab (nb090AlphaDummy780 v u h) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy778 v u h) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy778 v u h)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy780 v u h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0828 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy042 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy777 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0829 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy785 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy785 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy777 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0830 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy778 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0831 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy787 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy787 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h) (SemanticCore.Class.cv (nb090AlphaDummy778 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0832 (A : SemanticCore.Class) : nb090AlphaDummy042 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy785 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy785 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0833 (v u h : SemanticCore.Var) : nb090AlphaDummy044 v u h ∈ (SemanticCore.Class.cab (nb090AlphaDummy787 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy787 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0834 (A : SemanticCore.Class) : nb090AlphaDummy786 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy786 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0835 (v u h : SemanticCore.Var) : nb090AlphaDummy788 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy788 v u h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0837 (v u h : SemanticCore.Var) : nb090AlphaDummy795 v u h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy795 v u h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy795 v u h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy795 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0838 (A : SemanticCore.Class) : nb090AlphaDummy793 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy793 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0839 (v u h : SemanticCore.Var) : nb090AlphaDummy795 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy795 v u h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0840 (A : SemanticCore.Class) : nb090AlphaDummy800 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy800 A)) (SemanticCore.Class.cv (nb090AlphaDummy801 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy800 A)) (SemanticCore.Class.cv (nb090AlphaDummy801 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0841 (v u h : SemanticCore.Var) : nb090AlphaDummy803 v u h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy804 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy804 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0842 (A : SemanticCore.Class) : nb090AlphaDummy800 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy800 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy801 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0843 (v u h : SemanticCore.Var) : nb090AlphaDummy803 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy804 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0844 (A : SemanticCore.Class) : nb090AlphaDummy801 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy800 A)) (SemanticCore.Class.cv (nb090AlphaDummy801 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy800 A)) (SemanticCore.Class.cv (nb090AlphaDummy801 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0845 (v u h : SemanticCore.Var) : nb090AlphaDummy804 v u h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy804 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy804 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0846 (A : SemanticCore.Class) : nb090AlphaDummy801 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy800 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy801 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0847 (v u h : SemanticCore.Var) : nb090AlphaDummy804 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy804 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0848 (A : SemanticCore.Class) : nb090AlphaDummy800 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy800 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy801 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0849 (v u h : SemanticCore.Var) : nb090AlphaDummy803 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy803 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy804 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0850 (A : SemanticCore.Class) : nb090AlphaDummy800 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy800 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy800 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0851 (v u h : SemanticCore.Var) : nb090AlphaDummy803 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0852 (A : SemanticCore.Class) : nb090AlphaDummy801 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy800 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy801 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0853 (v u h : SemanticCore.Var) : nb090AlphaDummy804 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy803 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy804 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0854 (A : SemanticCore.Class) : nb090AlphaDummy801 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy801 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy801 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0855 (v u h : SemanticCore.Var) : nb090AlphaDummy804 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy804 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy804 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0856 (A : SemanticCore.Class) : nb090AlphaDummy777 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy042 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy777 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0857 (A : SemanticCore.Class) : nb090AlphaDummy777 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy785 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy785 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy777 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0858 (v u h : SemanticCore.Var) : nb090AlphaDummy778 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy778 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0859 (v u h : SemanticCore.Var) : nb090AlphaDummy778 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy787 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy787 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h) (SemanticCore.Class.cv (nb090AlphaDummy778 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0860 (A : SemanticCore.Class) : nb090AlphaDummy777 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy785 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy777 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy785 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy777 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0861 (v u h : SemanticCore.Var) : nb090AlphaDummy778 v u h ∈ (SemanticCore.Class.cab (nb090AlphaDummy787 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h) (SemanticCore.Class.cv (nb090AlphaDummy778 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy787 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h) (SemanticCore.Class.cv (nb090AlphaDummy778 v u h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0863 (v u h : SemanticCore.Var) : nb090AlphaDummy788 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0864 (A : SemanticCore.Class) : nb090AlphaDummy786 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0865 (v u h : SemanticCore.Var) : nb090AlphaDummy788 v u h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0866 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy699 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0867 (v u h : SemanticCore.Var) : h ∈ (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy701 v u h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h) (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0868 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy000 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy042 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0869 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ {nb090AlphaDummy777 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy777 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0870 (A : SemanticCore.Class) : nb090AlphaDummy000 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy779 A) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy777 A) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy777 A)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy779 A))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0871 (v u h : SemanticCore.Var) : h ∈ (SemanticCore.Class.cv h).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0872 (v u h : SemanticCore.Var) : h ∈ {nb090AlphaDummy778 v u h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy778 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0873 (v u h : SemanticCore.Var) : h ∈ (SemanticCore.Class.cab (nb090AlphaDummy780 v u h) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy778 v u h) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy778 v u h)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy780 v u h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0874 (A : SemanticCore.Class) : nb090AlphaDummy779 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy779 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0875 (v u h : SemanticCore.Var) : nb090AlphaDummy780 v u h ∈ (SemanticCore.Class.cv (nb090AlphaDummy780 v u h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0877 (v u h : SemanticCore.Var) : nb090AlphaDummy702 v u h ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0878 (A : SemanticCore.Class) : nb090AlphaDummy700 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0879 (v u h : SemanticCore.Var) : nb090AlphaDummy702 v u h ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0880 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy000 A)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy001 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy002 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy001 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0881 (v u h : SemanticCore.Var) : v ∈ (SemanticCore.Class.cv h).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0882 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ Compiler.CompactSourceSyntax.synC1st.fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy002 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0883 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ {nb090AlphaDummy827 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy002 A)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy827 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0884 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy829 A) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy827 A) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy002 A)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy827 A)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy829 A))))).fv

Certificates from NAR4C090C001Part022.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0885 (v : SemanticCore.Var) : v ∈ Compiler.CompactSourceSyntax.synC1st.fv ∪ (SemanticCore.Class.cv v).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0886 (v : SemanticCore.Var) : v ∈ {nb090AlphaDummy828 v} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv v) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy828 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0887 (v : SemanticCore.Var) : v ∈ (SemanticCore.Class.cab (nb090AlphaDummy830 v) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb090AlphaDummy828 v) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv v) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy828 v)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb090AlphaDummy830 v))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0888 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy002 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy827 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0889 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy835 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy836 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy835 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy835 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy836 A) (SemanticCore.Class.cv (nb090AlphaDummy827 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy835 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0890 (v : SemanticCore.Var) : v ∈ (SemanticCore.Class.cv v).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy828 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0891 (v : SemanticCore.Var) : v ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy837 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy838 v) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy837 v)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy837 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy838 v) (SemanticCore.Class.cv (nb090AlphaDummy828 v)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy837 v)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0892 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy835 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy836 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy835 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy835 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy836 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy835 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0893 (v : SemanticCore.Var) : v ∈ (SemanticCore.Class.cab (nb090AlphaDummy837 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy838 v) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy837 v)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v)))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy837 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy838 v) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy837 v)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0894 (A : SemanticCore.Class) : nb090AlphaDummy836 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy836 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0895 (v : SemanticCore.Var) : nb090AlphaDummy838 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy838 v)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0897 (v : SemanticCore.Var) : nb090AlphaDummy845 v ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy845 v)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb090AlphaDummy845 v)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy845 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0898 (A : SemanticCore.Class) : nb090AlphaDummy843 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy843 A)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0899 (v : SemanticCore.Var) : nb090AlphaDummy845 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy845 v)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0900 (A : SemanticCore.Class) : nb090AlphaDummy850 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy850 A)) (SemanticCore.Class.cv (nb090AlphaDummy851 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy850 A)) (SemanticCore.Class.cv (nb090AlphaDummy851 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0901 (v : SemanticCore.Var) : nb090AlphaDummy853 v ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy853 v)) (SemanticCore.Class.cv (nb090AlphaDummy854 v))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy853 v)) (SemanticCore.Class.cv (nb090AlphaDummy854 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0902 (A : SemanticCore.Class) : nb090AlphaDummy850 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy850 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy851 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0903 (v : SemanticCore.Var) : nb090AlphaDummy853 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy853 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy854 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0904 (A : SemanticCore.Class) : nb090AlphaDummy851 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy850 A)) (SemanticCore.Class.cv (nb090AlphaDummy851 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy850 A)) (SemanticCore.Class.cv (nb090AlphaDummy851 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0905 (v : SemanticCore.Var) : nb090AlphaDummy854 v ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy853 v)) (SemanticCore.Class.cv (nb090AlphaDummy854 v))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy853 v)) (SemanticCore.Class.cv (nb090AlphaDummy854 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0906 (A : SemanticCore.Class) : nb090AlphaDummy851 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy850 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy851 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0907 (v : SemanticCore.Var) : nb090AlphaDummy854 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy853 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy854 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0908 (A : SemanticCore.Class) : nb090AlphaDummy850 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy850 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy851 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0909 (v : SemanticCore.Var) : nb090AlphaDummy853 v ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy853 v))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy854 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0910 (A : SemanticCore.Class) : nb090AlphaDummy850 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy850 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy850 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0911 (v : SemanticCore.Var) : nb090AlphaDummy853 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy853 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy853 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0912 (A : SemanticCore.Class) : nb090AlphaDummy851 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy850 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy851 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0913 (v : SemanticCore.Var) : nb090AlphaDummy854 v ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy853 v))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy854 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0914 (A : SemanticCore.Class) : nb090AlphaDummy851 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy851 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy851 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0915 (v : SemanticCore.Var) : nb090AlphaDummy854 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy854 v)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy854 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0916 (A : SemanticCore.Class) : nb090AlphaDummy827 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy002 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy827 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0917 (A : SemanticCore.Class) : nb090AlphaDummy827 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy835 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy836 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy835 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy835 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy836 A) (SemanticCore.Class.cv (nb090AlphaDummy827 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy835 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0918 (v : SemanticCore.Var) : nb090AlphaDummy828 v ∈ (SemanticCore.Class.cv v).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy828 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0919 (v : SemanticCore.Var) : nb090AlphaDummy828 v ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy837 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy838 v) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy837 v)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy837 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy838 v) (SemanticCore.Class.cv (nb090AlphaDummy828 v)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy837 v)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0920 (A : SemanticCore.Class) : nb090AlphaDummy827 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy835 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy836 A) (SemanticCore.Class.cv (nb090AlphaDummy827 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy835 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy835 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy836 A) (SemanticCore.Class.cv (nb090AlphaDummy827 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy835 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0921 (v : SemanticCore.Var) : nb090AlphaDummy828 v ∈ (SemanticCore.Class.cab (nb090AlphaDummy837 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy838 v) (SemanticCore.Class.cv (nb090AlphaDummy828 v)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy837 v)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy837 v) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy838 v) (SemanticCore.Class.cv (nb090AlphaDummy828 v)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy837 v)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0923 (v : SemanticCore.Var) : nb090AlphaDummy838 v ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0924 (A : SemanticCore.Class) : nb090AlphaDummy836 A ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0925 (v : SemanticCore.Var) : nb090AlphaDummy838 v ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0926 (A : SemanticCore.Class) : nb090AlphaDummy829 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy829 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0927 (v : SemanticCore.Var) : nb090AlphaDummy830 v ∈ (SemanticCore.Class.cv (nb090AlphaDummy830 v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_compact_fv_empty_0020 (A : SemanticCore.Class) : nb090AlphaDummy002 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_compact_fv_empty_0021 (v : SemanticCore.Var) : v ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_compact_fv_empty_0022 (A : SemanticCore.Class) : nb090AlphaDummy001 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_compact_fv_empty_0023 (u : SemanticCore.Var) : u ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_compact_fv_empty_0024 (A : SemanticCore.Class) : nb090AlphaDummy003 A ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_compact_fv_empty_0025 (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) : nb090AlphaDummy004 v u A h ∉ ∅