Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C090C001Block004

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C090C001Part014.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_922 (A : SemanticCore.Class) :

nb090AlphaDummy271 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy262 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy263 A))).fv

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

nb090AlphaDummy272 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy265 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy266 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_924 (A : SemanticCore.Class) :

nb090AlphaDummy315 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy306 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy307 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_925 (u : SemanticCore.Var) :

nb090AlphaDummy316 u ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy309 u))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy310 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_926 (A : SemanticCore.Class) :

nb090AlphaDummy361 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy352 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy353 A))).fv

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

nb090AlphaDummy362 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy355 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy356 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_928 (A : SemanticCore.Class) :

nb090AlphaDummy405 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy396 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy397 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_929 (v : SemanticCore.Var) :

nb090AlphaDummy406 v ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy399 v))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy400 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_930 (A : SemanticCore.Class) :

nb090AlphaDummy455 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy446 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy447 A))).fv

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

nb090AlphaDummy456 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy449 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy450 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_932 (A : SemanticCore.Class) :

nb090AlphaDummy491 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy482 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy483 A))).fv

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

nb090AlphaDummy492 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy485 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy486 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_934 (A : SemanticCore.Class) :

nb090AlphaDummy533 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy524 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy525 A))).fv

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

nb090AlphaDummy534 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy527 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy528 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_936 (A : SemanticCore.Class) :

nb090AlphaDummy569 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy560 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy561 A))).fv

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

nb090AlphaDummy570 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy563 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy564 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_938 (A : SemanticCore.Class) :

nb090AlphaDummy605 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy596 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy597 A))).fv

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

nb090AlphaDummy606 h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy599 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy600 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_940 (A : SemanticCore.Class) :

nb090AlphaDummy641 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy632 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy633 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_941 (v u h : SemanticCore.Var) :

nb090AlphaDummy642 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy635 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy636 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_942 (A : SemanticCore.Class) :

nb090AlphaDummy685 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy676 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy677 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_943 (u : SemanticCore.Var) :

nb090AlphaDummy686 u ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy679 u))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy680 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_944 (A : SemanticCore.Class) :

nb090AlphaDummy739 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy730 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy731 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_945 (v u h : SemanticCore.Var) :

nb090AlphaDummy740 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy733 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy734 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_946 (A : SemanticCore.Class) :

nb090AlphaDummy769 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy760 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy761 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_947 (v u h : SemanticCore.Var) :

nb090AlphaDummy770 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy763 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy764 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_948 (A : SemanticCore.Class) :

nb090AlphaDummy809 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy800 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy801 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_949 (v u h : SemanticCore.Var) :

nb090AlphaDummy810 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy803 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy804 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_950 (A : SemanticCore.Class) :

nb090AlphaDummy859 A ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy850 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy851 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_951 (v : SemanticCore.Var) :

nb090AlphaDummy860 v ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy853 v))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy854 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_952 (A : SemanticCore.Class) :

nb090AlphaDummy037 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy006 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_953 (v u : SemanticCore.Var) :

nb090AlphaDummy038 v u ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_954 (A : SemanticCore.Class) :

nb090AlphaDummy089 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy058 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy090 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy060 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_956 (A : SemanticCore.Class) :

nb090AlphaDummy125 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy094 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy126 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy096 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_958 (A : SemanticCore.Class) :

nb090AlphaDummy167 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy168 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_960 (A : SemanticCore.Class) :

nb090AlphaDummy203 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy172 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy204 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy174 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_962 (A : SemanticCore.Class) :

nb090AlphaDummy239 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy240 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_964 (A : SemanticCore.Class) :

nb090AlphaDummy279 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy280 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_966 (A : SemanticCore.Class) :

nb090AlphaDummy323 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_967 (u : SemanticCore.Var) :

nb090AlphaDummy324 u ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_968 (A : SemanticCore.Class) :

nb090AlphaDummy369 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy370 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_970 (A : SemanticCore.Class) :

nb090AlphaDummy413 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_971 (v : SemanticCore.Var) :

nb090AlphaDummy414 v ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_972 (A : SemanticCore.Class) :

nb090AlphaDummy463 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy464 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_974 (A : SemanticCore.Class) :

nb090AlphaDummy499 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy500 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_976 (A : SemanticCore.Class) :

nb090AlphaDummy541 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy542 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_978 (A : SemanticCore.Class) :

nb090AlphaDummy577 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy578 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_980 (A : SemanticCore.Class) :

nb090AlphaDummy613 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

nb090AlphaDummy614 h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_982 (A : SemanticCore.Class) :

nb090AlphaDummy649 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_983 (v u h : SemanticCore.Var) :

nb090AlphaDummy650 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_984 (A : SemanticCore.Class) :

nb090AlphaDummy693 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_985 (u : SemanticCore.Var) :

nb090AlphaDummy694 u ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_986 (A : SemanticCore.Class) :

nb090AlphaDummy823 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_987 (v u h : SemanticCore.Var) :

nb090AlphaDummy824 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_988 (A : SemanticCore.Class) :

nb090AlphaDummy747 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_989 (v u h : SemanticCore.Var) :

nb090AlphaDummy748 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_990 (A : SemanticCore.Class) :

nb090AlphaDummy817 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_991 (v u h : SemanticCore.Var) :

nb090AlphaDummy818 v u h ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_992 (A : SemanticCore.Class) :

nb090AlphaDummy867 A ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_993 (v : SemanticCore.Var) :

nb090AlphaDummy868 v ∉ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_994 (A : SemanticCore.Class) :

nb090AlphaDummy699 A ∉ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_995 (A : SemanticCore.Class) :

nb090AlphaDummy700 A ∉ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy041 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy042 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_996 (A : SemanticCore.Class) :

nb090AlphaDummy699 A ≠ nb090AlphaDummy700 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_997 (v u h : SemanticCore.Var) :

nb090AlphaDummy701 v u h ∉ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_998 (v u h : SemanticCore.Var) :

nb090AlphaDummy702 v u h ∉ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy043 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy044 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_999 (v u h : SemanticCore.Var) :

nb090AlphaDummy701 v u h ≠ nb090AlphaDummy702 v u h

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1000 (A : SemanticCore.Class) :

nb090AlphaDummy025 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy020 A)) (SemanticCore.Class.cv (nb090AlphaDummy021 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy020 A)) (SemanticCore.Class.cv (nb090AlphaDummy021 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1001 (v u : SemanticCore.Var) :

nb090AlphaDummy026 v u ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy023 v u)) (SemanticCore.Class.cv (nb090AlphaDummy024 v u))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy023 v u)) (SemanticCore.Class.cv (nb090AlphaDummy024 v u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1002 (A : SemanticCore.Class) :

nb090AlphaDummy077 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy072 A)) (SemanticCore.Class.cv (nb090AlphaDummy073 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy072 A)) (SemanticCore.Class.cv (nb090AlphaDummy073 A))).fv

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

nb090AlphaDummy078 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy075 h)) (SemanticCore.Class.cv (nb090AlphaDummy076 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy075 h)) (SemanticCore.Class.cv (nb090AlphaDummy076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1004 (A : SemanticCore.Class) :

nb090AlphaDummy113 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy108 A)) (SemanticCore.Class.cv (nb090AlphaDummy109 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy108 A)) (SemanticCore.Class.cv (nb090AlphaDummy109 A))).fv

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

nb090AlphaDummy114 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy111 h)) (SemanticCore.Class.cv (nb090AlphaDummy112 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy111 h)) (SemanticCore.Class.cv (nb090AlphaDummy112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1006 (A : SemanticCore.Class) :

nb090AlphaDummy155 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy150 A)) (SemanticCore.Class.cv (nb090AlphaDummy151 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy150 A)) (SemanticCore.Class.cv (nb090AlphaDummy151 A))).fv

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

nb090AlphaDummy156 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy153 h)) (SemanticCore.Class.cv (nb090AlphaDummy154 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy153 h)) (SemanticCore.Class.cv (nb090AlphaDummy154 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1008 (A : SemanticCore.Class) :

nb090AlphaDummy191 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy186 A)) (SemanticCore.Class.cv (nb090AlphaDummy187 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy186 A)) (SemanticCore.Class.cv (nb090AlphaDummy187 A))).fv

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

nb090AlphaDummy192 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy189 h)) (SemanticCore.Class.cv (nb090AlphaDummy190 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy189 h)) (SemanticCore.Class.cv (nb090AlphaDummy190 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1010 (A : SemanticCore.Class) :

nb090AlphaDummy227 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy222 A)) (SemanticCore.Class.cv (nb090AlphaDummy223 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy222 A)) (SemanticCore.Class.cv (nb090AlphaDummy223 A))).fv

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

nb090AlphaDummy228 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy225 h)) (SemanticCore.Class.cv (nb090AlphaDummy226 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy225 h)) (SemanticCore.Class.cv (nb090AlphaDummy226 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1012 (A : SemanticCore.Class) :

nb090AlphaDummy267 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy262 A)) (SemanticCore.Class.cv (nb090AlphaDummy263 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy262 A)) (SemanticCore.Class.cv (nb090AlphaDummy263 A))).fv

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

nb090AlphaDummy268 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy265 h)) (SemanticCore.Class.cv (nb090AlphaDummy266 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy265 h)) (SemanticCore.Class.cv (nb090AlphaDummy266 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1014 (A : SemanticCore.Class) :

nb090AlphaDummy311 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy306 A)) (SemanticCore.Class.cv (nb090AlphaDummy307 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy306 A)) (SemanticCore.Class.cv (nb090AlphaDummy307 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1015 (u : SemanticCore.Var) :

nb090AlphaDummy312 u ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy309 u)) (SemanticCore.Class.cv (nb090AlphaDummy310 u))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy309 u)) (SemanticCore.Class.cv (nb090AlphaDummy310 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1016 (A : SemanticCore.Class) :

nb090AlphaDummy357 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy352 A)) (SemanticCore.Class.cv (nb090AlphaDummy353 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy352 A)) (SemanticCore.Class.cv (nb090AlphaDummy353 A))).fv

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

nb090AlphaDummy358 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy355 h)) (SemanticCore.Class.cv (nb090AlphaDummy356 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy355 h)) (SemanticCore.Class.cv (nb090AlphaDummy356 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1018 (A : SemanticCore.Class) :

nb090AlphaDummy401 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy396 A)) (SemanticCore.Class.cv (nb090AlphaDummy397 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy396 A)) (SemanticCore.Class.cv (nb090AlphaDummy397 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1019 (v : SemanticCore.Var) :

nb090AlphaDummy402 v ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy399 v)) (SemanticCore.Class.cv (nb090AlphaDummy400 v))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy399 v)) (SemanticCore.Class.cv (nb090AlphaDummy400 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1020 (A : SemanticCore.Class) :

nb090AlphaDummy451 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy446 A)) (SemanticCore.Class.cv (nb090AlphaDummy447 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy446 A)) (SemanticCore.Class.cv (nb090AlphaDummy447 A))).fv

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

nb090AlphaDummy452 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy449 h)) (SemanticCore.Class.cv (nb090AlphaDummy450 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy449 h)) (SemanticCore.Class.cv (nb090AlphaDummy450 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1022 (A : SemanticCore.Class) :

nb090AlphaDummy487 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy482 A)) (SemanticCore.Class.cv (nb090AlphaDummy483 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy482 A)) (SemanticCore.Class.cv (nb090AlphaDummy483 A))).fv

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

nb090AlphaDummy488 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy485 h)) (SemanticCore.Class.cv (nb090AlphaDummy486 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy485 h)) (SemanticCore.Class.cv (nb090AlphaDummy486 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1024 (A : SemanticCore.Class) :

nb090AlphaDummy529 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy524 A)) (SemanticCore.Class.cv (nb090AlphaDummy525 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy524 A)) (SemanticCore.Class.cv (nb090AlphaDummy525 A))).fv

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

nb090AlphaDummy530 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy527 h)) (SemanticCore.Class.cv (nb090AlphaDummy528 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy527 h)) (SemanticCore.Class.cv (nb090AlphaDummy528 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1026 (A : SemanticCore.Class) :

nb090AlphaDummy565 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy560 A)) (SemanticCore.Class.cv (nb090AlphaDummy561 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy560 A)) (SemanticCore.Class.cv (nb090AlphaDummy561 A))).fv

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

nb090AlphaDummy566 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy563 h)) (SemanticCore.Class.cv (nb090AlphaDummy564 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy563 h)) (SemanticCore.Class.cv (nb090AlphaDummy564 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1028 (A : SemanticCore.Class) :

nb090AlphaDummy601 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy596 A)) (SemanticCore.Class.cv (nb090AlphaDummy597 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy596 A)) (SemanticCore.Class.cv (nb090AlphaDummy597 A))).fv

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

nb090AlphaDummy602 h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy599 h)) (SemanticCore.Class.cv (nb090AlphaDummy600 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy599 h)) (SemanticCore.Class.cv (nb090AlphaDummy600 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1030 (A : SemanticCore.Class) :

nb090AlphaDummy637 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy632 A)) (SemanticCore.Class.cv (nb090AlphaDummy633 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy632 A)) (SemanticCore.Class.cv (nb090AlphaDummy633 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1031 (v u h : SemanticCore.Var) :

nb090AlphaDummy638 v u h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy636 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy635 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy636 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1032 (A : SemanticCore.Class) :

nb090AlphaDummy681 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy676 A)) (SemanticCore.Class.cv (nb090AlphaDummy677 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy676 A)) (SemanticCore.Class.cv (nb090AlphaDummy677 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1033 (u : SemanticCore.Var) :

nb090AlphaDummy682 u ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy679 u)) (SemanticCore.Class.cv (nb090AlphaDummy680 u))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy679 u)) (SemanticCore.Class.cv (nb090AlphaDummy680 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1034 (A : SemanticCore.Class) :

nb090AlphaDummy735 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy730 A)) (SemanticCore.Class.cv (nb090AlphaDummy731 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy730 A)) (SemanticCore.Class.cv (nb090AlphaDummy731 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1035 (v u h : SemanticCore.Var) :

nb090AlphaDummy736 v u h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy734 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy733 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy734 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1036 (A : SemanticCore.Class) :

nb090AlphaDummy765 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy760 A)) (SemanticCore.Class.cv (nb090AlphaDummy761 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy760 A)) (SemanticCore.Class.cv (nb090AlphaDummy761 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1037 (v u h : SemanticCore.Var) :

nb090AlphaDummy766 v u h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy764 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy763 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy764 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1038 (A : SemanticCore.Class) :

nb090AlphaDummy805 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy800 A)) (SemanticCore.Class.cv (nb090AlphaDummy801 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy800 A)) (SemanticCore.Class.cv (nb090AlphaDummy801 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1039 (v u h : SemanticCore.Var) :

nb090AlphaDummy806 v u h ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy804 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy803 v u h)) (SemanticCore.Class.cv (nb090AlphaDummy804 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1040 (A : SemanticCore.Class) :

nb090AlphaDummy855 A ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy850 A)) (SemanticCore.Class.cv (nb090AlphaDummy851 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy850 A)) (SemanticCore.Class.cv (nb090AlphaDummy851 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1041 (v : SemanticCore.Var) :

nb090AlphaDummy856 v ∉ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy853 v)) (SemanticCore.Class.cv (nb090AlphaDummy854 v))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy853 v)) (SemanticCore.Class.cv (nb090AlphaDummy854 v))).fv

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

nb090AlphaDummy046 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.nb090_fresh_1044 (A : SemanticCore.Class) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1047 (v h : SemanticCore.Var) :

nb090AlphaDummy330 v h ∉ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1048 (A : SemanticCore.Class) :

nb090AlphaDummy039 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy006 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy006 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1049 (v u : SemanticCore.Var) :

nb090AlphaDummy040 v u ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1050 (A : SemanticCore.Class) :

nb090AlphaDummy091 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy058 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy058 A))).fv

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

nb090AlphaDummy092 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy060 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy060 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1052 (A : SemanticCore.Class) :

nb090AlphaDummy127 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy094 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy094 A))).fv

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

nb090AlphaDummy128 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy096 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy096 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1054 (A : SemanticCore.Class) :

nb090AlphaDummy169 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))).fv

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

nb090AlphaDummy170 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1056 (A : SemanticCore.Class) :

nb090AlphaDummy205 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy172 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy172 A))).fv

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

nb090AlphaDummy206 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy174 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy174 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1058 (A : SemanticCore.Class) :

nb090AlphaDummy241 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A))).fv

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

nb090AlphaDummy242 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy210 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1060 (A : SemanticCore.Class) :

nb090AlphaDummy281 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy248 A))).fv

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

nb090AlphaDummy282 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy250 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1062 (A : SemanticCore.Class) :

nb090AlphaDummy325 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy292 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1063 (u : SemanticCore.Var) :

nb090AlphaDummy326 u ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy294 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1064 (A : SemanticCore.Class) :

nb090AlphaDummy371 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy338 A))).fv

Certificates from NAR4C090C001Part015.

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

nb090AlphaDummy372 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy340 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1066 (A : SemanticCore.Class) :

nb090AlphaDummy415 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy382 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1067 (v : SemanticCore.Var) :

nb090AlphaDummy416 v ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy384 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1068 (A : SemanticCore.Class) :

nb090AlphaDummy465 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy432 A))).fv

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

nb090AlphaDummy466 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy434 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1070 (A : SemanticCore.Class) :

nb090AlphaDummy501 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy468 A))).fv

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

nb090AlphaDummy502 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy470 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1072 (A : SemanticCore.Class) :

nb090AlphaDummy543 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy510 A))).fv

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

nb090AlphaDummy544 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy512 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1074 (A : SemanticCore.Class) :

nb090AlphaDummy579 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))).fv

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

nb090AlphaDummy580 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1076 (A : SemanticCore.Class) :

nb090AlphaDummy615 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy582 A))).fv

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

nb090AlphaDummy616 h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy584 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1078 (A : SemanticCore.Class) :

nb090AlphaDummy651 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy618 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1079 (v u h : SemanticCore.Var) :

nb090AlphaDummy652 v u h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy620 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1080 (A : SemanticCore.Class) :

nb090AlphaDummy695 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy662 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1081 (u : SemanticCore.Var) :

nb090AlphaDummy696 u ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy664 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1082 (A : SemanticCore.Class) :

nb090AlphaDummy825 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1083 (v u h : SemanticCore.Var) :

nb090AlphaDummy826 v u h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1084 (A : SemanticCore.Class) :

nb090AlphaDummy749 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy716 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1085 (v u h : SemanticCore.Var) :

nb090AlphaDummy750 v u h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy718 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1086 (A : SemanticCore.Class) :

nb090AlphaDummy819 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1087 (v u h : SemanticCore.Var) :

nb090AlphaDummy820 v u h ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1088 (A : SemanticCore.Class) :

nb090AlphaDummy869 A ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy836 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1089 (v : SemanticCore.Var) :

nb090AlphaDummy870 v ∉ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy838 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1090 (A : SemanticCore.Class) :

nb090AlphaDummy331 A ∉ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv (nb090AlphaDummy000 A))).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1091 (v h : SemanticCore.Var) :

nb090AlphaDummy332 v h ∉ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv h)).fv ∪ (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1092 (A : SemanticCore.Class) :

nb090AlphaDummy000 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1093 (A : SemanticCore.Class) :

nb090AlphaDummy001 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1094 (A : SemanticCore.Class) :

nb090AlphaDummy002 A ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_1095 (A : SemanticCore.Class) :

nb090AlphaDummy000 A ≠ nb090AlphaDummy001 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_1096 (A : SemanticCore.Class) :

nb090AlphaDummy000 A ≠ nb090AlphaDummy002 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_distinct_1097 (A : SemanticCore.Class) :

nb090AlphaDummy001 A ≠ nb090AlphaDummy002 A

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1098 (A : SemanticCore.Class) :

nb090AlphaDummy003 A ∉ {nb090AlphaDummy001 A} ∪ {nb090AlphaDummy002 A} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (Compiler.CompactSourceSyntax.synChwcodes A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (Compiler.CompactSourceSyntax.synChwcodes A))) (Compiler.CompactSourceSyntax.synWex (nb090AlphaDummy000 A) (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy001 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy002 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy001 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A)))))).fv

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

nb090AlphaDummy134 h ∉ {nb090AlphaDummy131 h} ∪ {nb090AlphaDummy132 h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy132 h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy131 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1103 (A : SemanticCore.Class) :

nb090AlphaDummy285 A ∉ {nb090AlphaDummy283 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy001 A)) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy283 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1104 (u : SemanticCore.Var) :

nb090AlphaDummy286 u ∉ {nb090AlphaDummy284 u} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy284 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1105 (A : SemanticCore.Class) :

nb090AlphaDummy375 A ∉ {nb090AlphaDummy373 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy002 A)) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy373 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1106 (v : SemanticCore.Var) :

nb090AlphaDummy376 v ∉ {nb090AlphaDummy374 v} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv v) Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy374 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1107 (A : SemanticCore.Class) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1111 (A : SemanticCore.Class) :

nb090AlphaDummy655 A ∉ {nb090AlphaDummy653 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy001 A)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy653 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1112 (u : SemanticCore.Var) :

nb090AlphaDummy656 u ∉ {nb090AlphaDummy654 u} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy654 u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1113 (A : SemanticCore.Class) :

nb090AlphaDummy709 A ∉ {nb090AlphaDummy707 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy041 A)) (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy707 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1114 (v u h : SemanticCore.Var) :

nb090AlphaDummy710 v u h ∉ {nb090AlphaDummy708 v u h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy043 v u h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy708 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1115 (A : SemanticCore.Class) :

nb090AlphaDummy779 A ∉ {nb090AlphaDummy777 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy042 A)) (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (SemanticCore.Class.cv (nb090AlphaDummy777 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1116 (v u h : SemanticCore.Var) :

nb090AlphaDummy780 v u h ∉ {nb090AlphaDummy778 v u h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy044 v u h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy778 v u h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1117 (A : SemanticCore.Class) :

nb090AlphaDummy829 A ∉ {nb090AlphaDummy827 A} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy002 A)) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy827 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1118 (v : SemanticCore.Var) :

nb090AlphaDummy830 v ∉ {nb090AlphaDummy828 v} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv v) Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy828 v))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_fresh_1119 (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) :

nb090AlphaDummy004 v u A h ∉ {u} ∪ {v} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcodes A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcodes A))) (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0000 (A : SemanticCore.Class) :

nb090AlphaDummy001 A ∈ {nb090AlphaDummy001 A} ∪ {nb090AlphaDummy002 A} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (Compiler.CompactSourceSyntax.synChwcodes A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (Compiler.CompactSourceSyntax.synChwcodes A))) (Compiler.CompactSourceSyntax.synWex (nb090AlphaDummy000 A) (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy001 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy002 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy001 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0001 (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) :

u ∈ {u} ∪ {v} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcodes A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcodes A))) (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0002 (A : SemanticCore.Class) :

nb090AlphaDummy002 A ∈ {nb090AlphaDummy001 A} ∪ {nb090AlphaDummy002 A} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (Compiler.CompactSourceSyntax.synChwcodes A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (Compiler.CompactSourceSyntax.synChwcodes A))) (Compiler.CompactSourceSyntax.synWex (nb090AlphaDummy000 A) (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv (nb090AlphaDummy000 A)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy001 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv (nb090AlphaDummy002 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy001 A))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv (nb090AlphaDummy002 A)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0003 (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) :

v ∈ {u} ∪ {v} ∪ (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcodes A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcodes A))) (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0004 (A : SemanticCore.Class) :

nb090AlphaDummy001 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy001 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy002 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0005 (A : SemanticCore.Class) :

nb090AlphaDummy001 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy005 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy006 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy005 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy006 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy005 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy006 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy005 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy006 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0006 (v u : SemanticCore.Var) :

u ∈ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv v).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0007 (v u : SemanticCore.Var) :

u ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy007 v u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy008 v u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy007 v u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy007 v u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy008 v u) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy007 v u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0008 (A : SemanticCore.Class) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0010 (A : SemanticCore.Class) :

nb090AlphaDummy006 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy006 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0011 (v u : SemanticCore.Var) :

nb090AlphaDummy008 v u ∈ (SemanticCore.Class.cv (nb090AlphaDummy008 v u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0014 (A : SemanticCore.Class) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0015 (v u : SemanticCore.Var) :

nb090AlphaDummy015 v u ∈ (SemanticCore.Class.cv (nb090AlphaDummy015 v u)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0016 (A : SemanticCore.Class) :

nb090AlphaDummy020 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy020 A)) (SemanticCore.Class.cv (nb090AlphaDummy021 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy020 A)) (SemanticCore.Class.cv (nb090AlphaDummy021 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0017 (v u : SemanticCore.Var) :

nb090AlphaDummy023 v u ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy023 v u)) (SemanticCore.Class.cv (nb090AlphaDummy024 v u))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy023 v u)) (SemanticCore.Class.cv (nb090AlphaDummy024 v u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0018 (A : SemanticCore.Class) :

nb090AlphaDummy020 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy020 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy021 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0019 (v u : SemanticCore.Var) :

nb090AlphaDummy023 v u ∈ (SemanticCore.Class.cv (nb090AlphaDummy023 v u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy024 v u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0020 (A : SemanticCore.Class) :

nb090AlphaDummy021 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy020 A)) (SemanticCore.Class.cv (nb090AlphaDummy021 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy020 A)) (SemanticCore.Class.cv (nb090AlphaDummy021 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0021 (v u : SemanticCore.Var) :

nb090AlphaDummy024 v u ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy023 v u)) (SemanticCore.Class.cv (nb090AlphaDummy024 v u))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy023 v u)) (SemanticCore.Class.cv (nb090AlphaDummy024 v u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0022 (A : SemanticCore.Class) :

nb090AlphaDummy021 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy020 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy021 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0023 (v u : SemanticCore.Var) :

nb090AlphaDummy024 v u ∈ (SemanticCore.Class.cv (nb090AlphaDummy023 v u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy024 v u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0024 (A : SemanticCore.Class) :

nb090AlphaDummy020 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy020 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy021 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0025 (v u : SemanticCore.Var) :

nb090AlphaDummy023 v u ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy023 v u))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy024 v u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0026 (A : SemanticCore.Class) :

nb090AlphaDummy020 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy020 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy020 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0027 (v u : SemanticCore.Var) :

nb090AlphaDummy023 v u ∈ (SemanticCore.Class.cv (nb090AlphaDummy023 v u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy023 v u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0028 (A : SemanticCore.Class) :

nb090AlphaDummy021 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy020 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy021 A))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0029 (v u : SemanticCore.Var) :

nb090AlphaDummy024 v u ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy023 v u))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy024 v u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0030 (A : SemanticCore.Class) :

nb090AlphaDummy021 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy021 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy021 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0031 (v u : SemanticCore.Var) :

nb090AlphaDummy024 v u ∈ (SemanticCore.Class.cv (nb090AlphaDummy024 v u)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy024 v u)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0032 (A : SemanticCore.Class) :

nb090AlphaDummy002 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy001 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy002 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0033 (A : SemanticCore.Class) :

nb090AlphaDummy002 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy005 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy006 A) (SemanticCore.Class.cv (nb090AlphaDummy001 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy005 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy006 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy005 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy006 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy005 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy006 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0034 (v u : SemanticCore.Var) :

v ∈ (SemanticCore.Class.cv u).fv ∪ (SemanticCore.Class.cv v).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0035 (v u : SemanticCore.Var) :

v ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy007 v u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy008 v u) (SemanticCore.Class.cv u) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy007 v u)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy007 v u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy008 v u) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy007 v u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0036 (A : SemanticCore.Class) :

nb090AlphaDummy002 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy005 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy006 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy005 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy006 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy005 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy006 A) (SemanticCore.Class.cv (nb090AlphaDummy002 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy005 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy006 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0037 (v u : SemanticCore.Var) :

v ∈ (SemanticCore.Class.cab (nb090AlphaDummy007 v u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy008 v u) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy007 v u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy007 v u) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy008 v u) (SemanticCore.Class.cv v) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy007 v u)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0038 (A : SemanticCore.Class) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0039 (v u : SemanticCore.Var) :

nb090AlphaDummy008 v u ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0040 (A : SemanticCore.Class) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0041 (v u : SemanticCore.Var) :

nb090AlphaDummy008 v u ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy008 v u))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0046 (A : SemanticCore.Class) :

nb090AlphaDummy049 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy049 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy050 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0047 (A : SemanticCore.Class) :

nb090AlphaDummy049 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy057 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy058 A) (SemanticCore.Class.cv (nb090AlphaDummy049 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy057 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy058 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy057 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy058 A) (SemanticCore.Class.cv (nb090AlphaDummy050 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy057 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy058 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb090AlphaDummy052 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy052 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy053 h)).fv

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

nb090AlphaDummy052 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy059 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy060 h) (SemanticCore.Class.cv (nb090AlphaDummy052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy059 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy060 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy059 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy060 h) (SemanticCore.Class.cv (nb090AlphaDummy053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy059 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy060 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0050 (A : SemanticCore.Class) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0052 (A : SemanticCore.Class) :

nb090AlphaDummy058 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy058 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0056 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0058 (A : SemanticCore.Class) :

nb090AlphaDummy072 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy072 A)) (SemanticCore.Class.cv (nb090AlphaDummy073 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy072 A)) (SemanticCore.Class.cv (nb090AlphaDummy073 A))).fv

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

nb090AlphaDummy075 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy075 h)) (SemanticCore.Class.cv (nb090AlphaDummy076 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy075 h)) (SemanticCore.Class.cv (nb090AlphaDummy076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0060 (A : SemanticCore.Class) :

nb090AlphaDummy072 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy072 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy073 A)).fv

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

nb090AlphaDummy075 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy075 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy076 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0062 (A : SemanticCore.Class) :

nb090AlphaDummy073 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy072 A)) (SemanticCore.Class.cv (nb090AlphaDummy073 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy072 A)) (SemanticCore.Class.cv (nb090AlphaDummy073 A))).fv

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

nb090AlphaDummy076 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy075 h)) (SemanticCore.Class.cv (nb090AlphaDummy076 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy075 h)) (SemanticCore.Class.cv (nb090AlphaDummy076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0064 (A : SemanticCore.Class) :

nb090AlphaDummy073 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy072 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy073 A)).fv

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

nb090AlphaDummy076 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy075 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy076 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0066 (A : SemanticCore.Class) :

nb090AlphaDummy072 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy072 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy073 A))).fv

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

nb090AlphaDummy075 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy075 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0068 (A : SemanticCore.Class) :

nb090AlphaDummy072 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy072 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy072 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0070 (A : SemanticCore.Class) :

nb090AlphaDummy073 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy072 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy073 A))).fv

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

nb090AlphaDummy076 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy075 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy076 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0072 (A : SemanticCore.Class) :

nb090AlphaDummy073 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy073 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy073 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0074 (A : SemanticCore.Class) :

nb090AlphaDummy050 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy049 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy050 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0075 (A : SemanticCore.Class) :

nb090AlphaDummy050 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy057 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy058 A) (SemanticCore.Class.cv (nb090AlphaDummy049 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy057 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy058 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy057 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy058 A) (SemanticCore.Class.cv (nb090AlphaDummy050 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy057 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy058 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb090AlphaDummy053 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy052 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy053 h)).fv

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

nb090AlphaDummy053 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy059 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy060 h) (SemanticCore.Class.cv (nb090AlphaDummy052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy059 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy060 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy059 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy060 h) (SemanticCore.Class.cv (nb090AlphaDummy053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy059 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy060 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0078 (A : SemanticCore.Class) :

nb090AlphaDummy050 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy057 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy058 A) (SemanticCore.Class.cv (nb090AlphaDummy050 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy057 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy058 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy057 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy058 A) (SemanticCore.Class.cv (nb090AlphaDummy050 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy057 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy058 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

Certificates from NAR4C090C001Part016.

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

nb090AlphaDummy053 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy059 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy060 h) (SemanticCore.Class.cv (nb090AlphaDummy053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy059 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy060 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy059 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy060 h) (SemanticCore.Class.cv (nb090AlphaDummy053 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy059 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy060 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0080 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0082 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0084 (A : SemanticCore.Class) :

nb090AlphaDummy049 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy049 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy051 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0085 (A : SemanticCore.Class) :

nb090AlphaDummy049 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy093 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy094 A) (SemanticCore.Class.cv (nb090AlphaDummy049 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy093 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy094 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy093 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy094 A) (SemanticCore.Class.cv (nb090AlphaDummy051 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy093 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy094 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb090AlphaDummy052 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy052 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy054 h)).fv

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

nb090AlphaDummy052 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy095 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy096 h) (SemanticCore.Class.cv (nb090AlphaDummy052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy095 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy096 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy095 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy096 h) (SemanticCore.Class.cv (nb090AlphaDummy054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy095 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy096 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0088 (A : SemanticCore.Class) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0090 (A : SemanticCore.Class) :

nb090AlphaDummy094 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy094 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0094 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0096 (A : SemanticCore.Class) :

nb090AlphaDummy108 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy108 A)) (SemanticCore.Class.cv (nb090AlphaDummy109 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy108 A)) (SemanticCore.Class.cv (nb090AlphaDummy109 A))).fv

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

nb090AlphaDummy111 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy111 h)) (SemanticCore.Class.cv (nb090AlphaDummy112 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy111 h)) (SemanticCore.Class.cv (nb090AlphaDummy112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0098 (A : SemanticCore.Class) :

nb090AlphaDummy108 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy108 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy109 A)).fv

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

nb090AlphaDummy111 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy111 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy112 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0100 (A : SemanticCore.Class) :

nb090AlphaDummy109 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy108 A)) (SemanticCore.Class.cv (nb090AlphaDummy109 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy108 A)) (SemanticCore.Class.cv (nb090AlphaDummy109 A))).fv

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

nb090AlphaDummy112 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy111 h)) (SemanticCore.Class.cv (nb090AlphaDummy112 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy111 h)) (SemanticCore.Class.cv (nb090AlphaDummy112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0102 (A : SemanticCore.Class) :

nb090AlphaDummy109 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy108 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy109 A)).fv

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

nb090AlphaDummy112 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy111 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy112 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0104 (A : SemanticCore.Class) :

nb090AlphaDummy108 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy108 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy109 A))).fv

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

nb090AlphaDummy111 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy111 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0106 (A : SemanticCore.Class) :

nb090AlphaDummy108 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy108 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy108 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0108 (A : SemanticCore.Class) :

nb090AlphaDummy109 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy108 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy109 A))).fv

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

nb090AlphaDummy112 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy111 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy112 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0110 (A : SemanticCore.Class) :

nb090AlphaDummy109 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy109 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy109 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0112 (A : SemanticCore.Class) :

nb090AlphaDummy051 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy049 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy051 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0113 (A : SemanticCore.Class) :

nb090AlphaDummy051 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy093 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy094 A) (SemanticCore.Class.cv (nb090AlphaDummy049 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy093 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy094 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy093 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy094 A) (SemanticCore.Class.cv (nb090AlphaDummy051 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy093 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy094 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb090AlphaDummy054 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy052 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy054 h)).fv

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

nb090AlphaDummy054 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy095 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy096 h) (SemanticCore.Class.cv (nb090AlphaDummy052 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy095 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy096 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy095 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy096 h) (SemanticCore.Class.cv (nb090AlphaDummy054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy095 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy096 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0116 (A : SemanticCore.Class) :

nb090AlphaDummy051 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy093 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy094 A) (SemanticCore.Class.cv (nb090AlphaDummy051 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy093 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy094 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy093 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy094 A) (SemanticCore.Class.cv (nb090AlphaDummy051 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy093 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy094 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb090AlphaDummy054 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy095 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy096 h) (SemanticCore.Class.cv (nb090AlphaDummy054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy095 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy096 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy095 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy096 h) (SemanticCore.Class.cv (nb090AlphaDummy054 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy095 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy096 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0118 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0120 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0126 (A : SemanticCore.Class) :

nb090AlphaDummy129 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy129 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy130 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0127 (A : SemanticCore.Class) :

nb090AlphaDummy129 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy135 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy136 A) (SemanticCore.Class.cv (nb090AlphaDummy129 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy135 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy135 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy136 A) (SemanticCore.Class.cv (nb090AlphaDummy130 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy135 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb090AlphaDummy131 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy131 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy132 h)).fv

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

nb090AlphaDummy131 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy137 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy138 h) (SemanticCore.Class.cv (nb090AlphaDummy131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy137 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy137 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy138 h) (SemanticCore.Class.cv (nb090AlphaDummy132 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy137 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0130 (A : SemanticCore.Class) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0132 (A : SemanticCore.Class) :

nb090AlphaDummy136 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy136 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0136 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0138 (A : SemanticCore.Class) :

nb090AlphaDummy150 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy150 A)) (SemanticCore.Class.cv (nb090AlphaDummy151 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy150 A)) (SemanticCore.Class.cv (nb090AlphaDummy151 A))).fv

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

nb090AlphaDummy153 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy153 h)) (SemanticCore.Class.cv (nb090AlphaDummy154 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy153 h)) (SemanticCore.Class.cv (nb090AlphaDummy154 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0140 (A : SemanticCore.Class) :

nb090AlphaDummy150 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy150 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy151 A)).fv

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

nb090AlphaDummy153 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy153 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy154 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0142 (A : SemanticCore.Class) :

nb090AlphaDummy151 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy150 A)) (SemanticCore.Class.cv (nb090AlphaDummy151 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy150 A)) (SemanticCore.Class.cv (nb090AlphaDummy151 A))).fv

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

nb090AlphaDummy154 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy153 h)) (SemanticCore.Class.cv (nb090AlphaDummy154 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy153 h)) (SemanticCore.Class.cv (nb090AlphaDummy154 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0144 (A : SemanticCore.Class) :

nb090AlphaDummy151 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy150 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy151 A)).fv

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

nb090AlphaDummy154 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy153 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy154 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0146 (A : SemanticCore.Class) :

nb090AlphaDummy150 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy150 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy151 A))).fv

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

nb090AlphaDummy153 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy153 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy154 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0148 (A : SemanticCore.Class) :

nb090AlphaDummy150 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy150 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy150 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0150 (A : SemanticCore.Class) :

nb090AlphaDummy151 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy150 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy151 A))).fv

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

nb090AlphaDummy154 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy153 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy154 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0152 (A : SemanticCore.Class) :

nb090AlphaDummy151 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy151 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy151 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0154 (A : SemanticCore.Class) :

nb090AlphaDummy130 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy129 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy130 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0155 (A : SemanticCore.Class) :

nb090AlphaDummy130 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy135 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy136 A) (SemanticCore.Class.cv (nb090AlphaDummy129 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy135 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy135 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy136 A) (SemanticCore.Class.cv (nb090AlphaDummy130 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy135 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb090AlphaDummy132 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy131 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy132 h)).fv

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

nb090AlphaDummy132 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy137 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy138 h) (SemanticCore.Class.cv (nb090AlphaDummy131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy137 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy137 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy138 h) (SemanticCore.Class.cv (nb090AlphaDummy132 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy137 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0158 (A : SemanticCore.Class) :

nb090AlphaDummy130 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy135 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy136 A) (SemanticCore.Class.cv (nb090AlphaDummy130 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy135 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy135 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy136 A) (SemanticCore.Class.cv (nb090AlphaDummy130 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy135 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb090AlphaDummy132 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy137 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy138 h) (SemanticCore.Class.cv (nb090AlphaDummy132 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy137 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy137 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy138 h) (SemanticCore.Class.cv (nb090AlphaDummy132 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy137 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0160 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0162 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0164 (A : SemanticCore.Class) :

nb090AlphaDummy130 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy130 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy129 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0165 (A : SemanticCore.Class) :

nb090AlphaDummy130 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy171 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy172 A) (SemanticCore.Class.cv (nb090AlphaDummy130 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy171 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy172 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy171 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy172 A) (SemanticCore.Class.cv (nb090AlphaDummy129 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy171 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy172 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb090AlphaDummy132 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy132 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy131 h)).fv

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

nb090AlphaDummy132 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy173 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy174 h) (SemanticCore.Class.cv (nb090AlphaDummy132 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy173 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy174 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy173 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy174 h) (SemanticCore.Class.cv (nb090AlphaDummy131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy173 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy174 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0168 (A : SemanticCore.Class) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0170 (A : SemanticCore.Class) :

nb090AlphaDummy172 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy172 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0174 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0176 (A : SemanticCore.Class) :

nb090AlphaDummy186 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy186 A)) (SemanticCore.Class.cv (nb090AlphaDummy187 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy186 A)) (SemanticCore.Class.cv (nb090AlphaDummy187 A))).fv

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

nb090AlphaDummy189 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy189 h)) (SemanticCore.Class.cv (nb090AlphaDummy190 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy189 h)) (SemanticCore.Class.cv (nb090AlphaDummy190 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0178 (A : SemanticCore.Class) :

nb090AlphaDummy186 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy186 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy187 A)).fv

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

nb090AlphaDummy189 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy189 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy190 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0180 (A : SemanticCore.Class) :

nb090AlphaDummy187 A ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy186 A)) (SemanticCore.Class.cv (nb090AlphaDummy187 A))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy186 A)) (SemanticCore.Class.cv (nb090AlphaDummy187 A))).fv

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

nb090AlphaDummy190 h ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy189 h)) (SemanticCore.Class.cv (nb090AlphaDummy190 h))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb090AlphaDummy189 h)) (SemanticCore.Class.cv (nb090AlphaDummy190 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0182 (A : SemanticCore.Class) :

nb090AlphaDummy187 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy186 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy187 A)).fv

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

nb090AlphaDummy190 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy189 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy190 h)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0184 (A : SemanticCore.Class) :

nb090AlphaDummy186 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy186 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy187 A))).fv

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

nb090AlphaDummy189 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy189 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy190 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0186 (A : SemanticCore.Class) :

nb090AlphaDummy186 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy186 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy186 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0188 (A : SemanticCore.Class) :

nb090AlphaDummy187 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy186 A))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy187 A))).fv

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

nb090AlphaDummy190 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy189 h))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb090AlphaDummy190 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0190 (A : SemanticCore.Class) :

nb090AlphaDummy187 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy187 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy187 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0192 (A : SemanticCore.Class) :

nb090AlphaDummy129 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy130 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy129 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0193 (A : SemanticCore.Class) :

nb090AlphaDummy129 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy171 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy172 A) (SemanticCore.Class.cv (nb090AlphaDummy130 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy171 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy172 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy171 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy172 A) (SemanticCore.Class.cv (nb090AlphaDummy129 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy171 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy172 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb090AlphaDummy131 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy132 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy131 h)).fv

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

nb090AlphaDummy131 h ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy173 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy174 h) (SemanticCore.Class.cv (nb090AlphaDummy132 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy173 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy174 h))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy173 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy174 h) (SemanticCore.Class.cv (nb090AlphaDummy131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy173 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy174 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0196 (A : SemanticCore.Class) :

nb090AlphaDummy129 A ∈ (SemanticCore.Class.cab (nb090AlphaDummy171 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy172 A) (SemanticCore.Class.cv (nb090AlphaDummy129 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy171 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy172 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy171 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy172 A) (SemanticCore.Class.cv (nb090AlphaDummy129 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy171 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy172 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb090AlphaDummy131 h ∈ (SemanticCore.Class.cab (nb090AlphaDummy173 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy174 h) (SemanticCore.Class.cv (nb090AlphaDummy131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy173 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy174 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb090AlphaDummy173 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy174 h) (SemanticCore.Class.cv (nb090AlphaDummy131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy173 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy174 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0198 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0200 (A : SemanticCore.Class) :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0203 (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.nb090_support_mem_0204 (A : SemanticCore.Class) :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0205 (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.nb090_support_mem_0206 (A : SemanticCore.Class) :

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

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

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

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

h ∈ {nb090AlphaDummy131 h} ∪ {nb090AlphaDummy132 h} ∪ (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb090AlphaDummy132 h)) (SemanticCore.Class.cv h) (SemanticCore.Class.cv (nb090AlphaDummy131 h))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0212 (A : SemanticCore.Class) :

nb090AlphaDummy000 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy000 A)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0214 (A : SemanticCore.Class) :

nb090AlphaDummy051 A ∈ (SemanticCore.Class.cv (nb090AlphaDummy051 A)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy050 A)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090_support_mem_0215 (A : SemanticCore.Class) :

nb090AlphaDummy051 A ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy207 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy208 A) (SemanticCore.Class.cv (nb090AlphaDummy051 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy207 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb090AlphaDummy207 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy208 A) (SemanticCore.Class.cv (nb090AlphaDummy050 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy207 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy208 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb090AlphaDummy054 h ∈ (SemanticCore.Class.cv (nb090AlphaDummy054 h)).fv ∪ (SemanticCore.Class.cv (nb090AlphaDummy053 h)).fv