---

Step * 1 of Lemma assert-has-src


1. i : Id
2. k : Knd
3. ↑has-src(i;k)
⊢ ↑isrcv(k)
BY
{ (DVar `k'
   THEN Repeat (((Unfolds ``has-src isrcv`` (-1)) THEN (Reduce (-1))))
   THEN Auto
   THEN Unfold `isrcv` 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:



1.  i  :  Id
2.  k  :  Knd
3.  \muparrow{}has-src(i;k)
\mvdash{}  \muparrow{}isrcv(k)


By

(DVar  `k'
  THEN  Repeat  (((Unfolds  ``has-src  isrcv``  (-1))  THEN  (Reduce  (-1))))
  THEN  Auto
  THEN  Unfold  `isrcv`  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index