---

Step * 1 of Lemma lnk-inv-one-one


1. l1 : IdLnk
2. l2 : IdLnk
3. lnk-inv(l1) = lnk-inv(l2) ∈ IdLnk
⊢ l1 = l2 ∈ IdLnk
BY
{ ((ApFunToHypEquands `Z' ⌈lnk-inv(Z)⌉ ⌈IdLnk⌉ (-1))⋅ THEN Auto THEN (RWO "lnk-inv-inv" (-1)) THEN Auto) }

---

Latex:



1.  l1  :  IdLnk
2.  l2  :  IdLnk
3.  lnk-inv(l1)  =  lnk-inv(l2)
\mvdash{}  l1  =  l2


By

((ApFunToHypEquands  `Z'  \mkleeneopen{}lnk-inv(Z)\mkleeneclose{}  \mkleeneopen{}IdLnk\mkleeneclose{}  (-1))\mcdot{}
  THEN  Auto
  THEN  (RWO  "lnk-inv-inv"  (-1))
  THEN  Auto)

---

Home Index