Step * of Lemma concat-cons

[l,ll:Top].  (concat([l ll]) concat(ll))
BY
(Auto THEN Unfold `concat` THEN Reduce THEN Auto) }


Latex:


Latex:
\mforall{}[l,ll:Top].    (concat([l  /  ll])  \msim{}  l  @  concat(ll))


By


Latex:
(Auto  THEN  Unfold  `concat`  0  THEN  Reduce  0  THEN  Auto)




Home Index