---

Step * of Lemma assert-isrcvl

∀[k:Knd]. ∀[l:IdLnk].  uiff(↑isrcvl(l;k);(↑isrcv(k)) ∧ (lnk(k) = l ∈ IdLnk))
BY
{ (BasicUniformUnivCD Auto THEN Unfold `isrcvl` 0⋅ THEN RepeatFor 2 (D 0) THEN Try (Complete (Auto))) }

1
1. k : Knd
2. l : IdLnk
3. ↑(isrcv(k) ∧b lnk(k) = l)
⊢ (↑isrcv(k)) ∧ (lnk(k) = l ∈ IdLnk)

---

Latex:


\mforall{}[k:Knd].  \mforall{}[l:IdLnk].    uiff(\muparrow{}isrcvl(l;k);(\muparrow{}isrcv(k))  \mwedge{}  (lnk(k)  =  l))


By

(BasicUniformUnivCD  Auto  THEN  Unfold  `isrcvl`  0\mcdot{}  THEN  RepeatFor  2  (D  0)  THEN  Try  (Complete  (Auto)))

---

Home Index