---

Step * of Lemma lnk-inv-inv

∀[l:IdLnk]. (lnk-inv(lnk-inv(l)) = l ∈ IdLnk)
BY
{ (Unfolds ``IdLnk lnk-inv`` 0 THEN Reduce 0 THEN Auto THEN (D (-1)) THEN (D (-1)) THEN Reduce 0 THEN Auto) }

---

Latex:


\mforall{}[l:IdLnk].  (lnk-inv(lnk-inv(l))  =  l)


By

(Unfolds  ``IdLnk  lnk-inv``  0
  THEN  Reduce  0
  THEN  Auto
  THEN  (D  (-1))
  THEN  (D  (-1))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index