Step
*
of Lemma
exception-type_wf
∀[T:Type]. (exception-type(T) ∈ Type)
BY
{ (Auto THEN Unfold `exception-type` 0 THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))) }
Latex:
Latex:
\mforall{}[T:Type].  (exception-type(T)  \mmember{}  Type)
By
Latex:
(Auto  THEN  Unfold  `exception-type`  0  THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto)))))
Home
Index