Nominal proof certificates grouped in dependency order.

Certificates from NAR4C078C001Part028.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0878 : nb078AlphaDummy847 ∈ {nb078AlphaDummy847} ∪ {nb078AlphaDummy848} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Class.cv nb078AlphaDummy002) (SemanticCore.Class.cv nb078AlphaDummy847)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0879 (h : SemanticCore.Var) : nb078AlphaDummy849 h ∈ {nb078AlphaDummy849 h} ∪ {nb078AlphaDummy850 h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb078AlphaDummy849 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0880 : nb078AlphaDummy848 ∈ {nb078AlphaDummy847} ∪ {nb078AlphaDummy848} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Class.cv nb078AlphaDummy002) (SemanticCore.Class.cv nb078AlphaDummy847)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0881 (h : SemanticCore.Var) : nb078AlphaDummy850 h ∈ {nb078AlphaDummy849 h} ∪ {nb078AlphaDummy850 h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb078AlphaDummy849 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0882 : nb078AlphaDummy847 ∈ (SemanticCore.Class.cv nb078AlphaDummy847).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy848).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0883 : nb078AlphaDummy847 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy853 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy854 (SemanticCore.Class.cv nb078AlphaDummy847) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy853) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy853 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy854 (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy853) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0884 (h : SemanticCore.Var) : nb078AlphaDummy849 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy849 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy850 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0885 (h : SemanticCore.Var) : nb078AlphaDummy849 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy855 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy856 h) (SemanticCore.Class.cv (nb078AlphaDummy849 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy855 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy855 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy856 h) (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy855 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0886 : nb078AlphaDummy847 ∈ (SemanticCore.Class.cab nb078AlphaDummy853 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy854 (SemanticCore.Class.cv nb078AlphaDummy847) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy853) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy853 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy854 (SemanticCore.Class.cv nb078AlphaDummy847) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy853) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0887 (h : SemanticCore.Var) : nb078AlphaDummy849 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy855 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy856 h) (SemanticCore.Class.cv (nb078AlphaDummy849 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy855 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy855 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy856 h) (SemanticCore.Class.cv (nb078AlphaDummy849 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy855 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0888 : nb078AlphaDummy854 ∈ (SemanticCore.Class.cv nb078AlphaDummy854).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0889 (h : SemanticCore.Var) : nb078AlphaDummy856 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy856 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0891 (h : SemanticCore.Var) : nb078AlphaDummy863 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy863 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy863 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy863 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0893 (h : SemanticCore.Var) : nb078AlphaDummy863 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy863 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0894 : nb078AlphaDummy868 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy868) (SemanticCore.Class.cv nb078AlphaDummy869)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy868) (SemanticCore.Class.cv nb078AlphaDummy869)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0895 (h : SemanticCore.Var) : nb078AlphaDummy871 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy871 h)) (SemanticCore.Class.cv (nb078AlphaDummy872 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy871 h)) (SemanticCore.Class.cv (nb078AlphaDummy872 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0896 : nb078AlphaDummy868 ∈ (SemanticCore.Class.cv nb078AlphaDummy868).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy869).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0897 (h : SemanticCore.Var) : nb078AlphaDummy871 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy871 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy872 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0898 : nb078AlphaDummy869 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy868) (SemanticCore.Class.cv nb078AlphaDummy869)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy868) (SemanticCore.Class.cv nb078AlphaDummy869)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0899 (h : SemanticCore.Var) : nb078AlphaDummy872 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy871 h)) (SemanticCore.Class.cv (nb078AlphaDummy872 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy871 h)) (SemanticCore.Class.cv (nb078AlphaDummy872 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0900 : nb078AlphaDummy869 ∈ (SemanticCore.Class.cv nb078AlphaDummy868).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy869).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0901 (h : SemanticCore.Var) : nb078AlphaDummy872 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy871 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy872 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0902 : nb078AlphaDummy868 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy868)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy869)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0903 (h : SemanticCore.Var) : nb078AlphaDummy871 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy871 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy872 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0904 : nb078AlphaDummy868 ∈ (SemanticCore.Class.cv nb078AlphaDummy868).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy868).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0905 (h : SemanticCore.Var) : nb078AlphaDummy871 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy871 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy871 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0906 : nb078AlphaDummy869 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy868)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy869)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0907 (h : SemanticCore.Var) : nb078AlphaDummy872 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy871 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy872 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0908 : nb078AlphaDummy869 ∈ (SemanticCore.Class.cv nb078AlphaDummy869).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy869).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0909 (h : SemanticCore.Var) : nb078AlphaDummy872 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy872 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy872 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0910 : nb078AlphaDummy848 ∈ (SemanticCore.Class.cv nb078AlphaDummy847).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy848).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0911 : nb078AlphaDummy848 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy853 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy854 (SemanticCore.Class.cv nb078AlphaDummy847) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy853) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy853 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy854 (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy853) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0912 (h : SemanticCore.Var) : nb078AlphaDummy850 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy849 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy850 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0913 (h : SemanticCore.Var) : nb078AlphaDummy850 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy855 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy856 h) (SemanticCore.Class.cv (nb078AlphaDummy849 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy855 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy855 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy856 h) (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy855 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0914 : nb078AlphaDummy848 ∈ (SemanticCore.Class.cab nb078AlphaDummy853 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy854 (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy853) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy853 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy854 (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy853) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy854)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0915 (h : SemanticCore.Var) : nb078AlphaDummy850 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy855 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy856 h) (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy855 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy855 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy856 h) (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy855 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy856 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0920 : nb078AlphaDummy848 ∈ (SemanticCore.Class.cv nb078AlphaDummy848).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy847).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0921 : nb078AlphaDummy848 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy889 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy890 (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy889) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy889 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy890 (SemanticCore.Class.cv nb078AlphaDummy847) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy889) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0922 (h : SemanticCore.Var) : nb078AlphaDummy850 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy850 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy849 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0923 (h : SemanticCore.Var) : nb078AlphaDummy850 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy891 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy892 h) (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy891 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy891 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy892 h) (SemanticCore.Class.cv (nb078AlphaDummy849 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy891 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0924 : nb078AlphaDummy848 ∈ (SemanticCore.Class.cab nb078AlphaDummy889 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy890 (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy889) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy889 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy890 (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy889) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0925 (h : SemanticCore.Var) : nb078AlphaDummy850 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy891 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy892 h) (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy891 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy891 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy892 h) (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy891 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0926 : nb078AlphaDummy890 ∈ (SemanticCore.Class.cv nb078AlphaDummy890).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0927 (h : SemanticCore.Var) : nb078AlphaDummy892 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy892 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0929 (h : SemanticCore.Var) : nb078AlphaDummy899 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy899 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy899 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy899 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0931 (h : SemanticCore.Var) : nb078AlphaDummy899 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy899 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0932 : nb078AlphaDummy904 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy904) (SemanticCore.Class.cv nb078AlphaDummy905)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy904) (SemanticCore.Class.cv nb078AlphaDummy905)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0933 (h : SemanticCore.Var) : nb078AlphaDummy907 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy907 h)) (SemanticCore.Class.cv (nb078AlphaDummy908 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy907 h)) (SemanticCore.Class.cv (nb078AlphaDummy908 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0934 : nb078AlphaDummy904 ∈ (SemanticCore.Class.cv nb078AlphaDummy904).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy905).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0935 (h : SemanticCore.Var) : nb078AlphaDummy907 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy907 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy908 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0936 : nb078AlphaDummy905 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy904) (SemanticCore.Class.cv nb078AlphaDummy905)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy904) (SemanticCore.Class.cv nb078AlphaDummy905)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0937 (h : SemanticCore.Var) : nb078AlphaDummy908 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy907 h)) (SemanticCore.Class.cv (nb078AlphaDummy908 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy907 h)) (SemanticCore.Class.cv (nb078AlphaDummy908 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0938 : nb078AlphaDummy905 ∈ (SemanticCore.Class.cv nb078AlphaDummy904).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy905).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0939 (h : SemanticCore.Var) : nb078AlphaDummy908 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy907 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy908 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0940 : nb078AlphaDummy904 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy904)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy905)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0941 (h : SemanticCore.Var) : nb078AlphaDummy907 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy907 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy908 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0942 : nb078AlphaDummy904 ∈ (SemanticCore.Class.cv nb078AlphaDummy904).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy904).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0943 (h : SemanticCore.Var) : nb078AlphaDummy907 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy907 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy907 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0944 : nb078AlphaDummy905 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy904)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy905)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0945 (h : SemanticCore.Var) : nb078AlphaDummy908 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy907 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy908 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0946 : nb078AlphaDummy905 ∈ (SemanticCore.Class.cv nb078AlphaDummy905).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy905).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0947 (h : SemanticCore.Var) : nb078AlphaDummy908 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy908 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy908 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0948 : nb078AlphaDummy847 ∈ (SemanticCore.Class.cv nb078AlphaDummy848).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy847).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0949 : nb078AlphaDummy847 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy889 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy890 (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy889) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy889 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy890 (SemanticCore.Class.cv nb078AlphaDummy847) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy889) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0950 (h : SemanticCore.Var) : nb078AlphaDummy849 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy850 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy849 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0951 (h : SemanticCore.Var) : nb078AlphaDummy849 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy891 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy892 h) (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy891 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy891 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy892 h) (SemanticCore.Class.cv (nb078AlphaDummy849 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy891 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0952 : nb078AlphaDummy847 ∈ (SemanticCore.Class.cab nb078AlphaDummy889 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy890 (SemanticCore.Class.cv nb078AlphaDummy847) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy889) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy889 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy890 (SemanticCore.Class.cv nb078AlphaDummy847) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy889) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy890)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0953 (h : SemanticCore.Var) : nb078AlphaDummy849 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy891 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy892 h) (SemanticCore.Class.cv (nb078AlphaDummy849 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy891 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy891 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy892 h) (SemanticCore.Class.cv (nb078AlphaDummy849 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy891 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy892 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

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

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

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

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0963 : nb078AlphaDummy002 ∈ {nb078AlphaDummy767} ∪ {nb078AlphaDummy768} ∪ (Compiler.CompactSourceSyntax.synWex nb078AlphaDummy769 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy767) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy769)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Class.cv nb078AlphaDummy002) (SemanticCore.Class.cv nb078AlphaDummy768)))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0965 (h : SemanticCore.Var) : h ∈ {nb078AlphaDummy770 h} ∪ {nb078AlphaDummy771 h} ∪ (Compiler.CompactSourceSyntax.synWex (nb078AlphaDummy772 h) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb078AlphaDummy772 h))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb078AlphaDummy771 h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0966 : nb078AlphaDummy002 ∈ {nb078AlphaDummy847} ∪ {nb078AlphaDummy848} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy848) (SemanticCore.Class.cv nb078AlphaDummy002) (SemanticCore.Class.cv nb078AlphaDummy847)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0967 (h : SemanticCore.Var) : h ∈ {nb078AlphaDummy849 h} ∪ {nb078AlphaDummy850 h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy850 h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb078AlphaDummy849 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0968 : nb078AlphaDummy002 ∈ (SemanticCore.Class.cv nb078AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0969 (h : SemanticCore.Var) : h ∈ (SemanticCore.Class.cv h).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0970 : nb078AlphaDummy769 ∈ (SemanticCore.Class.cv nb078AlphaDummy769).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy768).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0971 : nb078AlphaDummy769 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy925 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy926 (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy925) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy925 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy926 (SemanticCore.Class.cv nb078AlphaDummy768) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy925) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0972 (h : SemanticCore.Var) : nb078AlphaDummy772 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy772 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy771 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0973 (h : SemanticCore.Var) : nb078AlphaDummy772 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy927 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy928 h) (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy927 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy927 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy928 h) (SemanticCore.Class.cv (nb078AlphaDummy771 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy927 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0974 : nb078AlphaDummy769 ∈ (SemanticCore.Class.cab nb078AlphaDummy925 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy926 (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy925) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy925 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy926 (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy925) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0975 (h : SemanticCore.Var) : nb078AlphaDummy772 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy927 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy928 h) (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy927 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy927 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy928 h) (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy927 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0976 : nb078AlphaDummy926 ∈ (SemanticCore.Class.cv nb078AlphaDummy926).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0977 (h : SemanticCore.Var) : nb078AlphaDummy928 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy928 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0979 (h : SemanticCore.Var) : nb078AlphaDummy935 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy935 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy935 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy935 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0981 (h : SemanticCore.Var) : nb078AlphaDummy935 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy935 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0982 : nb078AlphaDummy940 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy940) (SemanticCore.Class.cv nb078AlphaDummy941)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy940) (SemanticCore.Class.cv nb078AlphaDummy941)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0983 (h : SemanticCore.Var) : nb078AlphaDummy943 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy943 h)) (SemanticCore.Class.cv (nb078AlphaDummy944 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy943 h)) (SemanticCore.Class.cv (nb078AlphaDummy944 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0984 : nb078AlphaDummy940 ∈ (SemanticCore.Class.cv nb078AlphaDummy940).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy941).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0985 (h : SemanticCore.Var) : nb078AlphaDummy943 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy943 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy944 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0986 : nb078AlphaDummy941 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy940) (SemanticCore.Class.cv nb078AlphaDummy941)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy940) (SemanticCore.Class.cv nb078AlphaDummy941)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0987 (h : SemanticCore.Var) : nb078AlphaDummy944 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy943 h)) (SemanticCore.Class.cv (nb078AlphaDummy944 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy943 h)) (SemanticCore.Class.cv (nb078AlphaDummy944 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0988 : nb078AlphaDummy941 ∈ (SemanticCore.Class.cv nb078AlphaDummy940).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy941).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0989 (h : SemanticCore.Var) : nb078AlphaDummy944 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy943 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy944 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0990 : nb078AlphaDummy940 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy940)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy941)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0991 (h : SemanticCore.Var) : nb078AlphaDummy943 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy943 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy944 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0992 : nb078AlphaDummy940 ∈ (SemanticCore.Class.cv nb078AlphaDummy940).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy940).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0993 (h : SemanticCore.Var) : nb078AlphaDummy943 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy943 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy943 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0994 : nb078AlphaDummy941 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy940)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy941)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0995 (h : SemanticCore.Var) : nb078AlphaDummy944 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy943 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy944 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0996 : nb078AlphaDummy941 ∈ (SemanticCore.Class.cv nb078AlphaDummy941).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy941).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0997 (h : SemanticCore.Var) : nb078AlphaDummy944 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy944 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy944 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0998 : nb078AlphaDummy768 ∈ (SemanticCore.Class.cv nb078AlphaDummy769).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy768).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_0999 : nb078AlphaDummy768 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy925 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy926 (SemanticCore.Class.cv nb078AlphaDummy769) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy925) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy925 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy926 (SemanticCore.Class.cv nb078AlphaDummy768) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy925) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1000 (h : SemanticCore.Var) : nb078AlphaDummy771 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy772 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy771 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1001 (h : SemanticCore.Var) : nb078AlphaDummy771 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy927 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy928 h) (SemanticCore.Class.cv (nb078AlphaDummy772 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy927 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy927 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy928 h) (SemanticCore.Class.cv (nb078AlphaDummy771 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy927 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1002 : nb078AlphaDummy768 ∈ (SemanticCore.Class.cab nb078AlphaDummy925 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy926 (SemanticCore.Class.cv nb078AlphaDummy768) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy925) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy925 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy926 (SemanticCore.Class.cv nb078AlphaDummy768) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy925) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy926)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1003 (h : SemanticCore.Var) : nb078AlphaDummy771 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy927 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy928 h) (SemanticCore.Class.cv (nb078AlphaDummy771 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy927 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy927 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy928 h) (SemanticCore.Class.cv (nb078AlphaDummy771 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy927 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy928 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1008 : nb078AlphaDummy962 ∈ (SemanticCore.Class.cv nb078AlphaDummy962).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy961).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1009 : nb078AlphaDummy962 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy965 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy966 (SemanticCore.Class.cv nb078AlphaDummy962) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy965) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy965 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy966 (SemanticCore.Class.cv nb078AlphaDummy961) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy965) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1010 (h : SemanticCore.Var) : nb078AlphaDummy964 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy964 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy963 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1011 (h : SemanticCore.Var) : nb078AlphaDummy964 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy967 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy968 h) (SemanticCore.Class.cv (nb078AlphaDummy964 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy967 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy967 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy968 h) (SemanticCore.Class.cv (nb078AlphaDummy963 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy967 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1012 : nb078AlphaDummy962 ∈ (SemanticCore.Class.cab nb078AlphaDummy965 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy966 (SemanticCore.Class.cv nb078AlphaDummy962) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy965) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy965 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy966 (SemanticCore.Class.cv nb078AlphaDummy962) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy965) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1013 (h : SemanticCore.Var) : nb078AlphaDummy964 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy967 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy968 h) (SemanticCore.Class.cv (nb078AlphaDummy964 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy967 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy967 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy968 h) (SemanticCore.Class.cv (nb078AlphaDummy964 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy967 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1014 : nb078AlphaDummy966 ∈ (SemanticCore.Class.cv nb078AlphaDummy966).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1015 (h : SemanticCore.Var) : nb078AlphaDummy968 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy968 h)).fv

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

Certificates from NAR4C078C001Part029.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1017 (h : SemanticCore.Var) : nb078AlphaDummy975 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy975 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy975 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy975 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1019 (h : SemanticCore.Var) : nb078AlphaDummy975 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy975 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1020 : nb078AlphaDummy980 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy980) (SemanticCore.Class.cv nb078AlphaDummy981)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy980) (SemanticCore.Class.cv nb078AlphaDummy981)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1021 (h : SemanticCore.Var) : nb078AlphaDummy983 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy983 h)) (SemanticCore.Class.cv (nb078AlphaDummy984 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy983 h)) (SemanticCore.Class.cv (nb078AlphaDummy984 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1022 : nb078AlphaDummy980 ∈ (SemanticCore.Class.cv nb078AlphaDummy980).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy981).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1023 (h : SemanticCore.Var) : nb078AlphaDummy983 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy983 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy984 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1024 : nb078AlphaDummy981 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy980) (SemanticCore.Class.cv nb078AlphaDummy981)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy980) (SemanticCore.Class.cv nb078AlphaDummy981)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1025 (h : SemanticCore.Var) : nb078AlphaDummy984 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy983 h)) (SemanticCore.Class.cv (nb078AlphaDummy984 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy983 h)) (SemanticCore.Class.cv (nb078AlphaDummy984 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1026 : nb078AlphaDummy981 ∈ (SemanticCore.Class.cv nb078AlphaDummy980).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy981).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1027 (h : SemanticCore.Var) : nb078AlphaDummy984 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy983 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy984 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1028 : nb078AlphaDummy980 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy980)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy981)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1029 (h : SemanticCore.Var) : nb078AlphaDummy983 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy983 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy984 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1030 : nb078AlphaDummy980 ∈ (SemanticCore.Class.cv nb078AlphaDummy980).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy980).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1031 (h : SemanticCore.Var) : nb078AlphaDummy983 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy983 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy983 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1032 : nb078AlphaDummy981 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy980)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy981)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1033 (h : SemanticCore.Var) : nb078AlphaDummy984 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy983 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy984 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1034 : nb078AlphaDummy981 ∈ (SemanticCore.Class.cv nb078AlphaDummy981).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy981).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1035 (h : SemanticCore.Var) : nb078AlphaDummy984 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy984 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy984 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1036 : nb078AlphaDummy961 ∈ (SemanticCore.Class.cv nb078AlphaDummy962).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy961).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1037 : nb078AlphaDummy961 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy965 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy966 (SemanticCore.Class.cv nb078AlphaDummy962) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy965) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy965 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy966 (SemanticCore.Class.cv nb078AlphaDummy961) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy965) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1038 (h : SemanticCore.Var) : nb078AlphaDummy963 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy964 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy963 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1039 (h : SemanticCore.Var) : nb078AlphaDummy963 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy967 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy968 h) (SemanticCore.Class.cv (nb078AlphaDummy964 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy967 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy967 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy968 h) (SemanticCore.Class.cv (nb078AlphaDummy963 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy967 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1040 : nb078AlphaDummy961 ∈ (SemanticCore.Class.cab nb078AlphaDummy965 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy966 (SemanticCore.Class.cv nb078AlphaDummy961) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy965) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy965 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy966 (SemanticCore.Class.cv nb078AlphaDummy961) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy965) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy966)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1041 (h : SemanticCore.Var) : nb078AlphaDummy963 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy967 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy968 h) (SemanticCore.Class.cv (nb078AlphaDummy963 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy967 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy967 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy968 h) (SemanticCore.Class.cv (nb078AlphaDummy963 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy967 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy968 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1046 : nb078AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1047 (h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1048 : nb078AlphaDummy1006 ∈ (SemanticCore.Class.cv nb078AlphaDummy1006).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1005).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1049 : nb078AlphaDummy1006 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1009 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1010 (SemanticCore.Class.cv nb078AlphaDummy1006) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1009) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1009 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1010 (SemanticCore.Class.cv nb078AlphaDummy1005) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1009) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1050 (h : SemanticCore.Var) : nb078AlphaDummy1008 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1008 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1007 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1051 (h : SemanticCore.Var) : nb078AlphaDummy1008 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1011 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1012 h) (SemanticCore.Class.cv (nb078AlphaDummy1008 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1011 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1011 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1012 h) (SemanticCore.Class.cv (nb078AlphaDummy1007 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1011 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1052 : nb078AlphaDummy1006 ∈ (SemanticCore.Class.cab nb078AlphaDummy1009 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1010 (SemanticCore.Class.cv nb078AlphaDummy1006) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1009) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy1009 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1010 (SemanticCore.Class.cv nb078AlphaDummy1006) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1009) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1053 (h : SemanticCore.Var) : nb078AlphaDummy1008 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy1011 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1012 h) (SemanticCore.Class.cv (nb078AlphaDummy1008 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1011 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy1011 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1012 h) (SemanticCore.Class.cv (nb078AlphaDummy1008 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1011 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1054 : nb078AlphaDummy1010 ∈ (SemanticCore.Class.cv nb078AlphaDummy1010).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1055 (h : SemanticCore.Var) : nb078AlphaDummy1012 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1012 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1057 (h : SemanticCore.Var) : nb078AlphaDummy1019 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1019 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1019 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1019 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1059 (h : SemanticCore.Var) : nb078AlphaDummy1019 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1019 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1060 : nb078AlphaDummy1024 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1024) (SemanticCore.Class.cv nb078AlphaDummy1025)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1024) (SemanticCore.Class.cv nb078AlphaDummy1025)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1061 (h : SemanticCore.Var) : nb078AlphaDummy1027 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1027 h)) (SemanticCore.Class.cv (nb078AlphaDummy1028 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1027 h)) (SemanticCore.Class.cv (nb078AlphaDummy1028 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1062 : nb078AlphaDummy1024 ∈ (SemanticCore.Class.cv nb078AlphaDummy1024).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1025).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1063 (h : SemanticCore.Var) : nb078AlphaDummy1027 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1027 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1028 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1064 : nb078AlphaDummy1025 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1024) (SemanticCore.Class.cv nb078AlphaDummy1025)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1024) (SemanticCore.Class.cv nb078AlphaDummy1025)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1065 (h : SemanticCore.Var) : nb078AlphaDummy1028 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1027 h)) (SemanticCore.Class.cv (nb078AlphaDummy1028 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1027 h)) (SemanticCore.Class.cv (nb078AlphaDummy1028 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1066 : nb078AlphaDummy1025 ∈ (SemanticCore.Class.cv nb078AlphaDummy1024).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1025).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1067 (h : SemanticCore.Var) : nb078AlphaDummy1028 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1027 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1028 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1068 : nb078AlphaDummy1024 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1024)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1025)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1069 (h : SemanticCore.Var) : nb078AlphaDummy1027 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1027 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1028 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1070 : nb078AlphaDummy1024 ∈ (SemanticCore.Class.cv nb078AlphaDummy1024).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1024).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1071 (h : SemanticCore.Var) : nb078AlphaDummy1027 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1027 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1027 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1072 : nb078AlphaDummy1025 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1024)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1025)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1073 (h : SemanticCore.Var) : nb078AlphaDummy1028 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1027 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1028 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1074 : nb078AlphaDummy1025 ∈ (SemanticCore.Class.cv nb078AlphaDummy1025).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1025).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1075 (h : SemanticCore.Var) : nb078AlphaDummy1028 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1028 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1028 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1076 : nb078AlphaDummy1005 ∈ (SemanticCore.Class.cv nb078AlphaDummy1006).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1005).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1077 : nb078AlphaDummy1005 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1009 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1010 (SemanticCore.Class.cv nb078AlphaDummy1006) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1009) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1009 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1010 (SemanticCore.Class.cv nb078AlphaDummy1005) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1009) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1078 (h : SemanticCore.Var) : nb078AlphaDummy1007 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1008 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1007 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1079 (h : SemanticCore.Var) : nb078AlphaDummy1007 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1011 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1012 h) (SemanticCore.Class.cv (nb078AlphaDummy1008 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1011 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1011 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1012 h) (SemanticCore.Class.cv (nb078AlphaDummy1007 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1011 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1080 : nb078AlphaDummy1005 ∈ (SemanticCore.Class.cab nb078AlphaDummy1009 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1010 (SemanticCore.Class.cv nb078AlphaDummy1005) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1009) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy1009 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1010 (SemanticCore.Class.cv nb078AlphaDummy1005) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1009) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1010)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1081 (h : SemanticCore.Var) : nb078AlphaDummy1007 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy1011 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1012 h) (SemanticCore.Class.cv (nb078AlphaDummy1007 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1011 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy1011 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1012 h) (SemanticCore.Class.cv (nb078AlphaDummy1007 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1011 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1012 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1086 : nb078AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy004)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy004)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1087 (y h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (SemanticCore.Class.cv y)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1088 : nb078AlphaDummy002 ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy002)).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy004).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1089 (y h : SemanticCore.Var) : h ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1090 : nb078AlphaDummy002 ∈ (SemanticCore.Class.cv nb078AlphaDummy002).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1091 (h : SemanticCore.Var) : h ∈ (SemanticCore.Class.cv h).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1092 : nb078AlphaDummy004 ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy004)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy004)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1093 (y h : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (SemanticCore.Class.cv y)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1094 : nb078AlphaDummy004 ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb078AlphaDummy002)).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy004).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1095 (y h : SemanticCore.Var) : y ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)).fv ∪ (SemanticCore.Class.cv y).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1096 : nb078AlphaDummy1049 ∈ {nb078AlphaDummy1049} ∪ {nb078AlphaDummy1050} ∪ (Compiler.CompactSourceSyntax.synWex nb078AlphaDummy1051 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy1049) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002))) (SemanticCore.Class.cv nb078AlphaDummy1051)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy1051) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy1050)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1097 (h : SemanticCore.Var) : nb078AlphaDummy1052 h ∈ {nb078AlphaDummy1052 h} ∪ {nb078AlphaDummy1053 h} ∪ (Compiler.CompactSourceSyntax.synWex (nb078AlphaDummy1054 h) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h))) (SemanticCore.Class.cv (nb078AlphaDummy1054 h))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy1054 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb078AlphaDummy1053 h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1098 : nb078AlphaDummy1050 ∈ {nb078AlphaDummy1049} ∪ {nb078AlphaDummy1050} ∪ (Compiler.CompactSourceSyntax.synWex nb078AlphaDummy1051 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy1049) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002))) (SemanticCore.Class.cv nb078AlphaDummy1051)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb078AlphaDummy1051) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb078AlphaDummy002)) (SemanticCore.Class.cv nb078AlphaDummy1050)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1099 (h : SemanticCore.Var) : nb078AlphaDummy1053 h ∈ {nb078AlphaDummy1052 h} ∪ {nb078AlphaDummy1053 h} ∪ (Compiler.CompactSourceSyntax.synWex (nb078AlphaDummy1054 h) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h))) (SemanticCore.Class.cv (nb078AlphaDummy1054 h))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb078AlphaDummy1054 h)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv h)) (SemanticCore.Class.cv (nb078AlphaDummy1053 h))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1100 : nb078AlphaDummy1049 ∈ (SemanticCore.Class.cv nb078AlphaDummy1049).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1050).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1101 : nb078AlphaDummy1049 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1057 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1058 (SemanticCore.Class.cv nb078AlphaDummy1049) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1057) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1057 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1058 (SemanticCore.Class.cv nb078AlphaDummy1050) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1057) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1102 (h : SemanticCore.Var) : nb078AlphaDummy1052 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1052 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1053 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1103 (h : SemanticCore.Var) : nb078AlphaDummy1052 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1059 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1060 h) (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1059 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1059 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1060 h) (SemanticCore.Class.cv (nb078AlphaDummy1053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1059 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1104 : nb078AlphaDummy1049 ∈ (SemanticCore.Class.cab nb078AlphaDummy1057 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1058 (SemanticCore.Class.cv nb078AlphaDummy1049) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1057) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy1057 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1058 (SemanticCore.Class.cv nb078AlphaDummy1049) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1057) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1105 (h : SemanticCore.Var) : nb078AlphaDummy1052 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy1059 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1060 h) (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1059 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy1059 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1060 h) (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1059 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1106 : nb078AlphaDummy1058 ∈ (SemanticCore.Class.cv nb078AlphaDummy1058).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1107 (h : SemanticCore.Var) : nb078AlphaDummy1060 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1060 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1109 (h : SemanticCore.Var) : nb078AlphaDummy1067 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1067 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1067 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1067 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1111 (h : SemanticCore.Var) : nb078AlphaDummy1067 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1067 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1112 : nb078AlphaDummy1072 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1072) (SemanticCore.Class.cv nb078AlphaDummy1073)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1072) (SemanticCore.Class.cv nb078AlphaDummy1073)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1113 (h : SemanticCore.Var) : nb078AlphaDummy1075 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1075 h)) (SemanticCore.Class.cv (nb078AlphaDummy1076 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1075 h)) (SemanticCore.Class.cv (nb078AlphaDummy1076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1114 : nb078AlphaDummy1072 ∈ (SemanticCore.Class.cv nb078AlphaDummy1072).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1073).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1115 (h : SemanticCore.Var) : nb078AlphaDummy1075 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1075 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1076 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1116 : nb078AlphaDummy1073 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1072) (SemanticCore.Class.cv nb078AlphaDummy1073)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1072) (SemanticCore.Class.cv nb078AlphaDummy1073)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1117 (h : SemanticCore.Var) : nb078AlphaDummy1076 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1075 h)) (SemanticCore.Class.cv (nb078AlphaDummy1076 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1075 h)) (SemanticCore.Class.cv (nb078AlphaDummy1076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1118 : nb078AlphaDummy1073 ∈ (SemanticCore.Class.cv nb078AlphaDummy1072).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1073).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1119 (h : SemanticCore.Var) : nb078AlphaDummy1076 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1075 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1076 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1120 : nb078AlphaDummy1072 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1072)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1073)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1121 (h : SemanticCore.Var) : nb078AlphaDummy1075 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1075 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1122 : nb078AlphaDummy1072 ∈ (SemanticCore.Class.cv nb078AlphaDummy1072).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1072).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1123 (h : SemanticCore.Var) : nb078AlphaDummy1075 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1075 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1075 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1124 : nb078AlphaDummy1073 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1072)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1073)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1125 (h : SemanticCore.Var) : nb078AlphaDummy1076 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1075 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1126 : nb078AlphaDummy1073 ∈ (SemanticCore.Class.cv nb078AlphaDummy1073).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1073).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1127 (h : SemanticCore.Var) : nb078AlphaDummy1076 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1076 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1076 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1128 : nb078AlphaDummy1050 ∈ (SemanticCore.Class.cv nb078AlphaDummy1049).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1050).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1129 : nb078AlphaDummy1050 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1057 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1058 (SemanticCore.Class.cv nb078AlphaDummy1049) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1057) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1057 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1058 (SemanticCore.Class.cv nb078AlphaDummy1050) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1057) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1130 (h : SemanticCore.Var) : nb078AlphaDummy1053 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1052 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1053 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1131 (h : SemanticCore.Var) : nb078AlphaDummy1053 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1059 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1060 h) (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1059 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1059 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1060 h) (SemanticCore.Class.cv (nb078AlphaDummy1053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1059 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1132 : nb078AlphaDummy1050 ∈ (SemanticCore.Class.cab nb078AlphaDummy1057 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1058 (SemanticCore.Class.cv nb078AlphaDummy1050) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1057) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy1057 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1058 (SemanticCore.Class.cv nb078AlphaDummy1050) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1057) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1058)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1133 (h : SemanticCore.Var) : nb078AlphaDummy1053 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy1059 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1060 h) (SemanticCore.Class.cv (nb078AlphaDummy1053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1059 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy1059 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1060 h) (SemanticCore.Class.cv (nb078AlphaDummy1053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1059 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1060 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1138 : nb078AlphaDummy1049 ∈ (SemanticCore.Class.cv nb078AlphaDummy1049).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1051).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1139 : nb078AlphaDummy1049 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1093 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1094 (SemanticCore.Class.cv nb078AlphaDummy1049) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1093) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1094)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb078AlphaDummy1093 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1094 (SemanticCore.Class.cv nb078AlphaDummy1051) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1093) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1094)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1140 (h : SemanticCore.Var) : nb078AlphaDummy1052 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1052 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1054 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1141 (h : SemanticCore.Var) : nb078AlphaDummy1052 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1095 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1096 h) (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1095 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1096 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb078AlphaDummy1095 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1096 h) (SemanticCore.Class.cv (nb078AlphaDummy1054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1095 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1096 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1142 : nb078AlphaDummy1049 ∈ (SemanticCore.Class.cab nb078AlphaDummy1093 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1094 (SemanticCore.Class.cv nb078AlphaDummy1049) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1093) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1094))))).fv ∪ (SemanticCore.Class.cab nb078AlphaDummy1093 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy1094 (SemanticCore.Class.cv nb078AlphaDummy1049) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy1093) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy1094))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1143 (h : SemanticCore.Var) : nb078AlphaDummy1052 h ∈ (SemanticCore.Class.cab (nb078AlphaDummy1095 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1096 h) (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1095 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1096 h)))))).fv ∪ (SemanticCore.Class.cab (nb078AlphaDummy1095 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy1096 h) (SemanticCore.Class.cv (nb078AlphaDummy1052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy1095 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy1096 h)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1144 : nb078AlphaDummy1094 ∈ (SemanticCore.Class.cv nb078AlphaDummy1094).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1145 (h : SemanticCore.Var) : nb078AlphaDummy1096 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1096 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1147 (h : SemanticCore.Var) : nb078AlphaDummy1103 h ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy1103 h)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb078AlphaDummy1103 h)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1103 h)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1149 (h : SemanticCore.Var) : nb078AlphaDummy1103 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1103 h)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1150 : nb078AlphaDummy1108 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1108) (SemanticCore.Class.cv nb078AlphaDummy1109)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1108) (SemanticCore.Class.cv nb078AlphaDummy1109)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1151 (h : SemanticCore.Var) : nb078AlphaDummy1111 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1111 h)) (SemanticCore.Class.cv (nb078AlphaDummy1112 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1111 h)) (SemanticCore.Class.cv (nb078AlphaDummy1112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1152 : nb078AlphaDummy1108 ∈ (SemanticCore.Class.cv nb078AlphaDummy1108).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1109).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1153 (h : SemanticCore.Var) : nb078AlphaDummy1111 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1111 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1112 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1154 : nb078AlphaDummy1109 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1108) (SemanticCore.Class.cv nb078AlphaDummy1109)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb078AlphaDummy1108) (SemanticCore.Class.cv nb078AlphaDummy1109)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1155 (h : SemanticCore.Var) : nb078AlphaDummy1112 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1111 h)) (SemanticCore.Class.cv (nb078AlphaDummy1112 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb078AlphaDummy1111 h)) (SemanticCore.Class.cv (nb078AlphaDummy1112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1156 : nb078AlphaDummy1109 ∈ (SemanticCore.Class.cv nb078AlphaDummy1108).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1109).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1157 (h : SemanticCore.Var) : nb078AlphaDummy1112 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1111 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1112 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1158 : nb078AlphaDummy1108 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1108)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1109)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1159 (h : SemanticCore.Var) : nb078AlphaDummy1111 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1111 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1160 : nb078AlphaDummy1108 ∈ (SemanticCore.Class.cv nb078AlphaDummy1108).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1108).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1161 (h : SemanticCore.Var) : nb078AlphaDummy1111 h ∈ (SemanticCore.Class.cv (nb078AlphaDummy1111 h)).fv ∪ (SemanticCore.Class.cv (nb078AlphaDummy1111 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1162 : nb078AlphaDummy1109 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1108)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb078AlphaDummy1109)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1163 (h : SemanticCore.Var) : nb078AlphaDummy1112 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1111 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb078AlphaDummy1112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078_support_mem_1164 : nb078AlphaDummy1109 ∈ (SemanticCore.Class.cv nb078AlphaDummy1109).fv ∪ (SemanticCore.Class.cv nb078AlphaDummy1109).fv