Documentation
LeanPool
.
NFWeakPartition
.
AlphaSupport
.
NAR4C078C001Part060Stage1
Search
return to top
source
Imports
Init
LeanPool.NFWeakPartition.NAR4C078C001Part059
Imported by
NFChoice
.
DirectNominalPrf
.
NominalAlphaWrappersRepaired
.
nb078_compact_fv_empty_0245
NF weak partition development: NAR4C078C001Part060.
source
theorem
NFChoice
.
DirectNominalPrf
.
NominalAlphaWrappersRepaired
.
nb078_compact_fv_empty_0245
(
g
:
SemanticCore.Var
)
:
g
∉
∅