Step 
*
 of Lemma 
decidable__equal_Kind
∀a,b:Knd.  Dec(a = b ∈ Knd)
BY
 
{ (RWO "assert-eq-knd<" 0 THEN Auto) }
 
Latex: 
Latex:
\mforall{}a,b:Knd.    Dec(a  =  b)
 By 
Latex:
(RWO  "assert-eq-knd<"  0  THEN  Auto)
Home
Index