Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C078C001Block007

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C078C001Part026.

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0598 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0600 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0602 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0604 :

nb078AlphaDummy592 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy592) (SemanticCore.Class.cv nb078AlphaDummy593)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy592) (SemanticCore.Class.cv nb078AlphaDummy593)).fv

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

nb078AlphaDummy595 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy595 g)) (SemanticCore.Class.cv (nb078AlphaDummy596 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy595 g)) (SemanticCore.Class.cv (nb078AlphaDummy596 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0606 :

nb078AlphaDummy592 ∈ (SemanticCore.Class.cv nb078AlphaDummy592).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy593).fv

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

nb078AlphaDummy595 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy595 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy596 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0608 :

nb078AlphaDummy593 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy592) (SemanticCore.Class.cv nb078AlphaDummy593)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy592) (SemanticCore.Class.cv nb078AlphaDummy593)).fv

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

nb078AlphaDummy596 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy595 g)) (SemanticCore.Class.cv (nb078AlphaDummy596 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy595 g)) (SemanticCore.Class.cv (nb078AlphaDummy596 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0610 :

nb078AlphaDummy593 ∈ (SemanticCore.Class.cv nb078AlphaDummy592).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy593).fv

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

nb078AlphaDummy596 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy595 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy596 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0612 :

nb078AlphaDummy592 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy592)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy593)).fv

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

nb078AlphaDummy595 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy595 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy596 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0614 :

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

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

nb078AlphaDummy595 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy595 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy595 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0616 :

nb078AlphaDummy593 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy592)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy593)).fv

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

nb078AlphaDummy596 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy595 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy596 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0618 :

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

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

nb078AlphaDummy596 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy596 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy596 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0620 :

nb078AlphaDummy570 ∈ (SemanticCore.Class.cv nb078AlphaDummy569).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy570).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0621 :

nb078AlphaDummy570 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy577 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy578 (SemanticCore.Class.cv nb078AlphaDummy569) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy577) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy577 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy578 (SemanticCore.Class.cv nb078AlphaDummy570) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy577) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb078AlphaDummy573 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy572 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy573 g)).fv

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

nb078AlphaDummy573 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy579 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy580 g) (SemanticCore.Class.cv (nb078AlphaDummy572 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy579 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy579 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy580 g) (SemanticCore.Class.cv (nb078AlphaDummy573 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy579 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0624 :

nb078AlphaDummy570 ∈ (SemanticCore.Class.cab nb078AlphaDummy577 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy578 (SemanticCore.Class.cv nb078AlphaDummy570) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy577) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy577 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy578 (SemanticCore.Class.cv nb078AlphaDummy570) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy577) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy578)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb078AlphaDummy573 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy579 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy580 g) (SemanticCore.Class.cv (nb078AlphaDummy573 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy579 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy579 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy580 g) (SemanticCore.Class.cv (nb078AlphaDummy573 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy579 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy580 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0626 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0628 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0630 :

nb078AlphaDummy569 ∈ (SemanticCore.Class.cv nb078AlphaDummy569).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy571).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0631 :

nb078AlphaDummy569 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy613 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy614 (SemanticCore.Class.cv nb078AlphaDummy569) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy613) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy613 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy614 (SemanticCore.Class.cv nb078AlphaDummy571) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy613) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb078AlphaDummy572 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy572 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy574 g)).fv

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

nb078AlphaDummy572 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy615 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy616 g) (SemanticCore.Class.cv (nb078AlphaDummy572 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy615 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy615 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy616 g) (SemanticCore.Class.cv (nb078AlphaDummy574 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy615 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0636 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0638 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0640 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0642 :

nb078AlphaDummy628 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy628) (SemanticCore.Class.cv nb078AlphaDummy629)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy628) (SemanticCore.Class.cv nb078AlphaDummy629)).fv

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

nb078AlphaDummy631 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy631 g)) (SemanticCore.Class.cv (nb078AlphaDummy632 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy631 g)) (SemanticCore.Class.cv (nb078AlphaDummy632 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0644 :

nb078AlphaDummy628 ∈ (SemanticCore.Class.cv nb078AlphaDummy628).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy629).fv

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

nb078AlphaDummy631 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy631 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy632 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0646 :

nb078AlphaDummy629 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy628) (SemanticCore.Class.cv nb078AlphaDummy629)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy628) (SemanticCore.Class.cv nb078AlphaDummy629)).fv

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

nb078AlphaDummy632 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy631 g)) (SemanticCore.Class.cv (nb078AlphaDummy632 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy631 g)) (SemanticCore.Class.cv (nb078AlphaDummy632 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0648 :

nb078AlphaDummy629 ∈ (SemanticCore.Class.cv nb078AlphaDummy628).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy629).fv

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

nb078AlphaDummy632 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy631 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy632 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0650 :

nb078AlphaDummy628 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy628)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy629)).fv

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

nb078AlphaDummy631 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy631 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy632 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0652 :

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

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

nb078AlphaDummy631 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy631 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy631 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0654 :

nb078AlphaDummy629 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy628)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy629)).fv

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

nb078AlphaDummy632 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy631 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy632 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0656 :

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

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

nb078AlphaDummy632 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy632 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy632 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0658 :

nb078AlphaDummy571 ∈ (SemanticCore.Class.cv nb078AlphaDummy569).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy571).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0659 :

nb078AlphaDummy571 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy613 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy614 (SemanticCore.Class.cv nb078AlphaDummy569) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy613) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy613 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy614 (SemanticCore.Class.cv nb078AlphaDummy571) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy613) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb078AlphaDummy574 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy572 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy574 g)).fv

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

nb078AlphaDummy574 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy615 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy616 g) (SemanticCore.Class.cv (nb078AlphaDummy572 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy615 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy615 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy616 g) (SemanticCore.Class.cv (nb078AlphaDummy574 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy615 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0662 :

nb078AlphaDummy571 ∈ (SemanticCore.Class.cab nb078AlphaDummy613 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy614 (SemanticCore.Class.cv nb078AlphaDummy571) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy613) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy613 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy614 (SemanticCore.Class.cv nb078AlphaDummy571) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy613) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy614)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb078AlphaDummy574 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy615 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy616 g) (SemanticCore.Class.cv (nb078AlphaDummy574 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy615 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy615 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy616 g) (SemanticCore.Class.cv (nb078AlphaDummy574 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy615 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy616 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0664 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0666 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0672 :

nb078AlphaDummy649 ∈ (SemanticCore.Class.cv nb078AlphaDummy649).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy650).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0673 :

nb078AlphaDummy649 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy655 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy656 (SemanticCore.Class.cv nb078AlphaDummy649) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy655) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy656)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy655 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy656 (SemanticCore.Class.cv nb078AlphaDummy650) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy655) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy656)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb078AlphaDummy651 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy651 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy652 g)).fv

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

nb078AlphaDummy651 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy657 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy658 g) (SemanticCore.Class.cv (nb078AlphaDummy651 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy657 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy658 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy657 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy658 g) (SemanticCore.Class.cv (nb078AlphaDummy652 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy657 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy658 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0678 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0680 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0682 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0684 :

nb078AlphaDummy670 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy670) (SemanticCore.Class.cv nb078AlphaDummy671)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy670) (SemanticCore.Class.cv nb078AlphaDummy671)).fv

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

nb078AlphaDummy673 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy673 g)) (SemanticCore.Class.cv (nb078AlphaDummy674 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy673 g)) (SemanticCore.Class.cv (nb078AlphaDummy674 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0686 :

nb078AlphaDummy670 ∈ (SemanticCore.Class.cv nb078AlphaDummy670).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy671).fv

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

nb078AlphaDummy673 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy673 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy674 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0688 :

nb078AlphaDummy671 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy670) (SemanticCore.Class.cv nb078AlphaDummy671)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy670) (SemanticCore.Class.cv nb078AlphaDummy671)).fv

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

nb078AlphaDummy674 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy673 g)) (SemanticCore.Class.cv (nb078AlphaDummy674 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy673 g)) (SemanticCore.Class.cv (nb078AlphaDummy674 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0690 :

nb078AlphaDummy671 ∈ (SemanticCore.Class.cv nb078AlphaDummy670).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy671).fv

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

nb078AlphaDummy674 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy673 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy674 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0692 :

nb078AlphaDummy670 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy670)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy671)).fv

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

nb078AlphaDummy673 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy673 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy674 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0694 :

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

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

nb078AlphaDummy673 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy673 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy673 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0696 :

nb078AlphaDummy671 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy670)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy671)).fv

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

nb078AlphaDummy674 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy673 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy674 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0698 :

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

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

nb078AlphaDummy674 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy674 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy674 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0700 :

nb078AlphaDummy650 ∈ (SemanticCore.Class.cv nb078AlphaDummy649).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy650).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0701 :

nb078AlphaDummy650 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy655 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy656 (SemanticCore.Class.cv nb078AlphaDummy649) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy655) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy656)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy655 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy656 (SemanticCore.Class.cv nb078AlphaDummy650) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy655) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy656)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb078AlphaDummy652 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy651 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy652 g)).fv

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

nb078AlphaDummy652 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy657 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy658 g) (SemanticCore.Class.cv (nb078AlphaDummy651 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy657 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy658 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy657 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy658 g) (SemanticCore.Class.cv (nb078AlphaDummy652 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy657 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy658 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0704 :

nb078AlphaDummy650 ∈ (SemanticCore.Class.cab nb078AlphaDummy655 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy656 (SemanticCore.Class.cv nb078AlphaDummy650) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy655) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy656)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy655 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy656 (SemanticCore.Class.cv nb078AlphaDummy650) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy655) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy656)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb078AlphaDummy652 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy657 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy658 g) (SemanticCore.Class.cv (nb078AlphaDummy652 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy657 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy658 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy657 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy658 g) (SemanticCore.Class.cv (nb078AlphaDummy652 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy657 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy658 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0706 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0708 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0710 :

nb078AlphaDummy650 ∈ (SemanticCore.Class.cv nb078AlphaDummy650).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy649).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0711 :

nb078AlphaDummy650 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy691 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy692 (SemanticCore.Class.cv nb078AlphaDummy650) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy691) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy692)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy691 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy692 (SemanticCore.Class.cv nb078AlphaDummy649) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy691) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy692)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb078AlphaDummy652 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy652 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy651 g)).fv

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

nb078AlphaDummy652 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy693 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy694 g) (SemanticCore.Class.cv (nb078AlphaDummy652 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy693 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy694 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy693 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy694 g) (SemanticCore.Class.cv (nb078AlphaDummy651 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy693 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy694 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0716 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0718 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0720 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0722 :

nb078AlphaDummy706 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy706) (SemanticCore.Class.cv nb078AlphaDummy707)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy706) (SemanticCore.Class.cv nb078AlphaDummy707)).fv

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

nb078AlphaDummy709 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy709 g)) (SemanticCore.Class.cv (nb078AlphaDummy710 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy709 g)) (SemanticCore.Class.cv (nb078AlphaDummy710 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0724 :

nb078AlphaDummy706 ∈ (SemanticCore.Class.cv nb078AlphaDummy706).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy707).fv

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

nb078AlphaDummy709 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy709 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy710 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0726 :

nb078AlphaDummy707 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy706) (SemanticCore.Class.cv nb078AlphaDummy707)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy706) (SemanticCore.Class.cv nb078AlphaDummy707)).fv

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

nb078AlphaDummy710 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy709 g)) (SemanticCore.Class.cv (nb078AlphaDummy710 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy709 g)) (SemanticCore.Class.cv (nb078AlphaDummy710 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0728 :

nb078AlphaDummy707 ∈ (SemanticCore.Class.cv nb078AlphaDummy706).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy707).fv

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

nb078AlphaDummy710 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy709 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy710 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0730 :

nb078AlphaDummy706 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy706)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy707)).fv

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

nb078AlphaDummy709 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy709 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy710 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0732 :

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

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

nb078AlphaDummy709 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy709 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy709 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0734 :

nb078AlphaDummy707 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy706)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy707)).fv

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

nb078AlphaDummy710 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy709 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy710 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0736 :

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

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

nb078AlphaDummy710 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy710 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy710 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0738 :

nb078AlphaDummy649 ∈ (SemanticCore.Class.cv nb078AlphaDummy650).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy649).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0739 :

nb078AlphaDummy649 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy691 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy692 (SemanticCore.Class.cv nb078AlphaDummy650) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy691) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy692)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy691 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy692 (SemanticCore.Class.cv nb078AlphaDummy649) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy691) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy692)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb078AlphaDummy651 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy652 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy651 g)).fv

Certificates from NAR4C078C001Part027.

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

nb078AlphaDummy651 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy693 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy694 g) (SemanticCore.Class.cv (nb078AlphaDummy652 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy693 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy694 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy693 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy694 g) (SemanticCore.Class.cv (nb078AlphaDummy651 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy693 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy694 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0742 :

nb078AlphaDummy649 ∈ (SemanticCore.Class.cab nb078AlphaDummy691 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy692 (SemanticCore.Class.cv nb078AlphaDummy649) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy691) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy692)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy691 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy692 (SemanticCore.Class.cv nb078AlphaDummy649) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy691) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy692)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb078AlphaDummy651 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy693 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy694 g) (SemanticCore.Class.cv (nb078AlphaDummy651 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy693 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy694 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy693 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy694 g) (SemanticCore.Class.cv (nb078AlphaDummy651 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy693 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy694 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0744 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0746 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0748 :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0750 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0752 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0758 :

nb078AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy001)).fv

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

g ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0760 :

nb078AlphaDummy571 ∈ (SemanticCore.Class.cv nb078AlphaDummy571).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy570).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0761 :

nb078AlphaDummy571 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy727 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy728 (SemanticCore.Class.cv nb078AlphaDummy571) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy727) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy728)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy727 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy728 (SemanticCore.Class.cv nb078AlphaDummy570) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy727) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy728)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb078AlphaDummy574 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy574 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy573 g)).fv

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

nb078AlphaDummy574 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy729 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy730 g) (SemanticCore.Class.cv (nb078AlphaDummy574 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy729 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy730 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy729 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy730 g) (SemanticCore.Class.cv (nb078AlphaDummy573 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy729 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy730 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0766 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0768 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0770 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0772 :

nb078AlphaDummy742 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy742) (SemanticCore.Class.cv nb078AlphaDummy743)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy742) (SemanticCore.Class.cv nb078AlphaDummy743)).fv

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

nb078AlphaDummy745 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy745 g)) (SemanticCore.Class.cv (nb078AlphaDummy746 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy745 g)) (SemanticCore.Class.cv (nb078AlphaDummy746 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0774 :

nb078AlphaDummy742 ∈ (SemanticCore.Class.cv nb078AlphaDummy742).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy743).fv

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

nb078AlphaDummy745 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy745 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy746 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0776 :

nb078AlphaDummy743 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy742) (SemanticCore.Class.cv nb078AlphaDummy743)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy742) (SemanticCore.Class.cv nb078AlphaDummy743)).fv

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

nb078AlphaDummy746 g ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy745 g)) (SemanticCore.Class.cv (nb078AlphaDummy746 g))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy745 g)) (SemanticCore.Class.cv (nb078AlphaDummy746 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0778 :

nb078AlphaDummy743 ∈ (SemanticCore.Class.cv nb078AlphaDummy742).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy743).fv

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

nb078AlphaDummy746 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy745 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy746 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0780 :

nb078AlphaDummy742 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy742)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy743)).fv

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

nb078AlphaDummy745 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy745 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy746 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0782 :

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

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

nb078AlphaDummy745 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy745 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy745 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0784 :

nb078AlphaDummy743 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy742)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy743)).fv

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

nb078AlphaDummy746 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy745 g))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy746 g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0786 :

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

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

nb078AlphaDummy746 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy746 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy746 g)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0788 :

nb078AlphaDummy570 ∈ (SemanticCore.Class.cv nb078AlphaDummy571).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy570).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0789 :

nb078AlphaDummy570 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy727 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy728 (SemanticCore.Class.cv nb078AlphaDummy571) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy727) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy728)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy727 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy728 (SemanticCore.Class.cv nb078AlphaDummy570) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy727) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy728)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb078AlphaDummy573 g ∈ (SemanticCore.Class.cv (nb078AlphaDummy574 g)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy573 g)).fv

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

nb078AlphaDummy573 g ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy729 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy730 g) (SemanticCore.Class.cv (nb078AlphaDummy574 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy729 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy730 g))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy729 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy730 g) (SemanticCore.Class.cv (nb078AlphaDummy573 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy729 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy730 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0792 :

nb078AlphaDummy570 ∈ (SemanticCore.Class.cab nb078AlphaDummy727 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy728 (SemanticCore.Class.cv nb078AlphaDummy570) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy727) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy728)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy727 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy728 (SemanticCore.Class.cv nb078AlphaDummy570) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy727) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy728)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb078AlphaDummy573 g ∈ (SemanticCore.Class.cab (nb078AlphaDummy729 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy730 g) (SemanticCore.Class.cv (nb078AlphaDummy573 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy729 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy730 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy729 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy730 g) (SemanticCore.Class.cv (nb078AlphaDummy573 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy729 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy730 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0794 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0796 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0802 :

nb078AlphaDummy767 ∈ (SemanticCore.Class.cv nb078AlphaDummy767).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy768).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0803 :

nb078AlphaDummy767 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy775 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy776 (SemanticCore.Class.cv nb078AlphaDummy767) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy775) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy775 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy776 (SemanticCore.Class.cv nb078AlphaDummy768) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy775) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0804 (h : SemanticCore.Var) :

nb078AlphaDummy770 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy770 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy771 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0805 (h : SemanticCore.Var) :

nb078AlphaDummy770 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy777 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy778 h) (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy777 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy777 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy778 h) (SemanticCore.Class.cv (nb078AlphaDummy771 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy777 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0807 (h : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0808 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0809 (h : SemanticCore.Var) :

nb078AlphaDummy778 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy778 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0810 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0812 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0813 (h : SemanticCore.Var) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0814 :

nb078AlphaDummy790 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy790) (SemanticCore.Class.cv nb078AlphaDummy791)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy790) (SemanticCore.Class.cv nb078AlphaDummy791)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0815 (h : SemanticCore.Var) :

nb078AlphaDummy793 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy793 h)) (SemanticCore.Class.cv (nb078AlphaDummy794 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy793 h)) (SemanticCore.Class.cv (nb078AlphaDummy794 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0816 :

nb078AlphaDummy790 ∈ (SemanticCore.Class.cv nb078AlphaDummy790).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy791).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0817 (h : SemanticCore.Var) :

nb078AlphaDummy793 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy793 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy794 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0818 :

nb078AlphaDummy791 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy790) (SemanticCore.Class.cv nb078AlphaDummy791)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy790) (SemanticCore.Class.cv nb078AlphaDummy791)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0819 (h : SemanticCore.Var) :

nb078AlphaDummy794 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy793 h)) (SemanticCore.Class.cv (nb078AlphaDummy794 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy793 h)) (SemanticCore.Class.cv (nb078AlphaDummy794 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0820 :

nb078AlphaDummy791 ∈ (SemanticCore.Class.cv nb078AlphaDummy790).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy791).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0821 (h : SemanticCore.Var) :

nb078AlphaDummy794 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy793 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy794 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0822 :

nb078AlphaDummy790 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy790)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy791)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0823 (h : SemanticCore.Var) :

nb078AlphaDummy793 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy793 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy794 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0824 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0825 (h : SemanticCore.Var) :

nb078AlphaDummy793 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy793 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy793 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0826 :

nb078AlphaDummy791 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy790)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy791)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0827 (h : SemanticCore.Var) :

nb078AlphaDummy794 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy793 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy794 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0828 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0829 (h : SemanticCore.Var) :

nb078AlphaDummy794 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy794 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy794 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0830 :

nb078AlphaDummy768 ∈ (SemanticCore.Class.cv nb078AlphaDummy767).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy768).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0831 :

nb078AlphaDummy768 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy775 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy776 (SemanticCore.Class.cv nb078AlphaDummy767) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy775) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy775 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy776 (SemanticCore.Class.cv nb078AlphaDummy768) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy775) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0832 (h : SemanticCore.Var) :

nb078AlphaDummy771 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy770 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy771 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0833 (h : SemanticCore.Var) :

nb078AlphaDummy771 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy777 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy778 h) (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy777 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy777 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy778 h) (SemanticCore.Class.cv (nb078AlphaDummy771 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy777 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0834 :

nb078AlphaDummy768 ∈ (SemanticCore.Class.cab nb078AlphaDummy775 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy776 (SemanticCore.Class.cv nb078AlphaDummy768) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy775) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy775 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy776 (SemanticCore.Class.cv nb078AlphaDummy768) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy775) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0835 (h : SemanticCore.Var) :

nb078AlphaDummy771 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy777 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy778 h) (SemanticCore.Class.cv (nb078AlphaDummy771 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy777 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy777 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy778 h) (SemanticCore.Class.cv (nb078AlphaDummy771 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy777 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0836 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0837 (h : SemanticCore.Var) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0838 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0839 (h : SemanticCore.Var) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0840 :

nb078AlphaDummy767 ∈ (SemanticCore.Class.cv nb078AlphaDummy767).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy769).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0841 :

nb078AlphaDummy767 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy811 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy812 (SemanticCore.Class.cv nb078AlphaDummy767) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy811) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy811 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy812 (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy811) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0842 (h : SemanticCore.Var) :

nb078AlphaDummy770 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy770 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy772 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0843 (h : SemanticCore.Var) :

nb078AlphaDummy770 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy813 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy814 h) (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy813 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy813 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy814 h) (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy813 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0845 (h : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0846 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0847 (h : SemanticCore.Var) :

nb078AlphaDummy814 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy814 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0848 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0850 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0851 (h : SemanticCore.Var) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0852 :

nb078AlphaDummy826 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy826) (SemanticCore.Class.cv nb078AlphaDummy827)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy826) (SemanticCore.Class.cv nb078AlphaDummy827)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0853 (h : SemanticCore.Var) :

nb078AlphaDummy829 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy829 h)) (SemanticCore.Class.cv (nb078AlphaDummy830 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy829 h)) (SemanticCore.Class.cv (nb078AlphaDummy830 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0854 :

nb078AlphaDummy826 ∈ (SemanticCore.Class.cv nb078AlphaDummy826).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy827).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0855 (h : SemanticCore.Var) :

nb078AlphaDummy829 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy829 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy830 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0856 :

nb078AlphaDummy827 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy826) (SemanticCore.Class.cv nb078AlphaDummy827)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy826) (SemanticCore.Class.cv nb078AlphaDummy827)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0857 (h : SemanticCore.Var) :

nb078AlphaDummy830 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy829 h)) (SemanticCore.Class.cv (nb078AlphaDummy830 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy829 h)) (SemanticCore.Class.cv (nb078AlphaDummy830 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0858 :

nb078AlphaDummy827 ∈ (SemanticCore.Class.cv nb078AlphaDummy826).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy827).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0859 (h : SemanticCore.Var) :

nb078AlphaDummy830 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy829 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy830 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0860 :

nb078AlphaDummy826 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy826)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy827)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0861 (h : SemanticCore.Var) :

nb078AlphaDummy829 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy829 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy830 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0862 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0863 (h : SemanticCore.Var) :

nb078AlphaDummy829 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy829 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy829 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0864 :

nb078AlphaDummy827 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy826)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy827)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0865 (h : SemanticCore.Var) :

nb078AlphaDummy830 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy829 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy830 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0866 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0867 (h : SemanticCore.Var) :

nb078AlphaDummy830 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy830 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy830 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0868 :

nb078AlphaDummy769 ∈ (SemanticCore.Class.cv nb078AlphaDummy767).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy769).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0869 :

nb078AlphaDummy769 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy811 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy812 (SemanticCore.Class.cv nb078AlphaDummy767) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy811) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy811 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy812 (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy811) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0870 (h : SemanticCore.Var) :

nb078AlphaDummy772 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy770 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy772 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0871 (h : SemanticCore.Var) :

nb078AlphaDummy772 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy813 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy814 h) (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy813 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy813 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy814 h) (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy813 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0872 :

nb078AlphaDummy769 ∈ (SemanticCore.Class.cab nb078AlphaDummy811 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy812 (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy811) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy811 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy812 (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy811) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0873 (h : SemanticCore.Var) :

nb078AlphaDummy772 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy813 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy814 h) (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy813 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy813 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy814 h) (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy813 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0874 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0875 (h : SemanticCore.Var) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0876 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0877 (h : SemanticCore.Var) :

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