---

Step * of Lemma locl_one_one

∀[a,b:Id].  a = b ∈ Id supposing locl(a) = locl(b) ∈ Knd
BY
{ (Unfolds ``Knd locl`` 0 THEN Auto) }

---

Latex:


\mforall{}[a,b:Id].    a  =  b  supposing  locl(a)  =  locl(b)


By

(Unfolds  ``Knd  locl``  0  THEN  Auto)

---

Home Index