Step
*
of Lemma
equipollent_same
∀[A:Type]. A ~ A
BY
{ ((Auto THEN RelRST) THEN Auto) }
Latex:
Latex:
\mforall{}[A:Type]. A \msim{} A
By
Latex:
((Auto THEN RelRST) THEN Auto)
Home
Index