---

Step * of Lemma lnk-inv-one-one

∀[l1,l2:IdLnk].  uiff(lnk-inv(l1) = lnk-inv(l2) ∈ IdLnk;l1 = l2 ∈ IdLnk)
BY
{ Auto ⋅ }

1
1. l1 : IdLnk
2. l2 : IdLnk
3. lnk-inv(l1) = lnk-inv(l2) ∈ IdLnk
⊢ l1 = l2 ∈ IdLnk

---

Latex:


\mforall{}[l1,l2:IdLnk].    uiff(lnk-inv(l1)  =  lnk-inv(l2);l1  =  l2)


By

Auto  \mcdot{}

---

Home Index