Step
*
of Lemma
equipollent-general-subtract-one
∀a:ℕ. ∀[T:Type]. (T ~ ℕa
⇒ (∀i:T. {x:T| ¬(x = i ∈ T)} ~ ℕa - 1))
BY
{ (Auto THEN BLemma `equipollent-subtract2` THEN Auto) }
Latex:
Latex:
\mforall{}a:\mBbbN{}. \mforall{}[T:Type]. (T \msim{} \mBbbN{}a {}\mRightarrow{} (\mforall{}i:T. \{x:T| \mneg{}(x = i)\} \msim{} \mBbbN{}a - 1))
By
Latex:
(Auto THEN BLemma `equipollent-subtract2` THEN Auto)
Home
Index