Step
*
of Lemma
decidable-equality-implies-Leibniz-type
∀T:Type. ((∀x,y:T. Dec(x = y ∈ T))
⇒ Leibniz-type{i:l}(T))
BY
{ (Auto THEN D 0 With ⌜λx,y. (¬(x = y ∈ T))⌝ THEN Reduce 0 THEN Auto THEN SupposeNot THEN Auto) }
Latex:
Latex:
\mforall{}T:Type. ((\mforall{}x,y:T. Dec(x = y)) {}\mRightarrow{} Leibniz-type\{i:l\}(T))
By
Latex:
(Auto THEN D 0 With \mkleeneopen{}\mlambda{}x,y. (\mneg{}(x = y))\mkleeneclose{} THEN Reduce 0 THEN Auto THEN SupposeNot THEN Auto)
Home
Index