Documentation
LeanPool
.
MatchingLogic
.
EntryIII
.
CanonicalConstruction
Search
return to top
source
Imports
Init
LeanPool.MatchingLogic.EntryIII.CanonicalChoice
LeanPool.MatchingLogic.EntryIII.CanonicalExistence
LeanPool.MatchingLogic.EntryIII.WitnessElim
Imported by
MatchingLogic
.
canonicalExistence
MatchingLogic.EntryIII.CanonicalConstruction
#
source
theorem
MatchingLogic
.
canonicalExistence
{
S
:
Signature
}
[
Countable
(
Pattern
S
ℕ
)
]
:
CanonicalExistenceProperty
S