Step
*
of Lemma
find-combine-nil
∀[cmp:Top]. (find-combine(cmp;[]) ~ inr ⋅ )
BY
{ (RepUR ``find-combine`` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[cmp:Top].  (find-combine(cmp;[])  \msim{}  inr  \mcdot{}  )
By
Latex:
(RepUR  ``find-combine``  0  THEN  Auto)
Home
Index