 187
 188/-! ## Certificate -/
 189
 190structure UniversalInstantiationCert (K : Type u) [Nonempty K] : Prop where
 191  instantiate :
 192    (∃ x y : K, x ≠ y) → Nonempty (LogicRealization.{u, 0})
 193  named :
 194    (∃ x y : K, x ≠ y) →
 195      ∃ x y : K, ∃ hxy : x ≠ y,
 196        Nonempty (LogicRealization.{u, 0})
 197
 198theorem universalInstantiationCert
 199    (K : Type u) [Nonempty K] :
 200    UniversalInstantiationCert K where
 201  instantiate := exists_logicRealization_of_distinction K
 202  named := exists_named_logicRealization_of_distinction K
 203
 204end UniversalInstantiationFromDistinction
 205end Foundation
 206end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.