Step 
*
 of Lemma 
es-causl-swellfnd
∀es:EO. SWellFounded((e < e'))
BY
 
{ (InstLemma `es-causl-swellfnd-base` []⋅ THEN RepeatFor 5 (ParallelLast)) }
 
Latex: 
\mforall{}es:EO.  SWellFounded((e  <  e'))
 By 
(InstLemma  `es-causl-swellfnd-base`  []\mcdot{}  THEN  RepeatFor  5  (ParallelLast))
Home
Index