Step * of Lemma decidable__equal_Kind

a,b:Knd.  Dec(a b ∈ Knd)
BY
(RWO "assert-eq-knd<THEN Auto) }


Latex:


Latex:
\mforall{}a,b:Knd.    Dec(a  =  b)


By


Latex:
(RWO  "assert-eq-knd<"  0  THEN  Auto)




Home Index