---

Step * of Lemma lnk-decl-dom2

∀[l,l2:IdLnk]. ∀[dt:tg:Id fp-> Type]. ∀[tg:Id].  l2 = l ∈ IdLnk supposing ↑rcv(l2,tg) ∈ dom(lnk-decl(l;dt))
BY
{ ((((UnivCD THENA Auto)
     THEN D 3
     THEN (Unfolds ``lnk-decl fpf-dom`` (-1))
     THEN (Reduce (-1))
     THEN (RWO "assert-deq-member" (-1)))
    THENA Auto
    )
   THEN (All (RWO "member_map"))
   THEN Auto
   THEN All Reduce
   THEN ExRepD
   THEN (FLemma `rcv_one_one` [(-1)])
   THEN Auto) }

---

Latex:


\mforall{}[l,l2:IdLnk].  \mforall{}[dt:tg:Id  fp->  Type].  \mforall{}[tg:Id].    l2  =  l  supposing  \muparrow{}rcv(l2,tg)  \mmember{}  dom(lnk-decl(l;dt))


By

((((UnivCD  THENA  Auto)
      THEN  D  3
      THEN  (Unfolds  ``lnk-decl  fpf-dom``  (-1))
      THEN  (Reduce  (-1))
      THEN  (RWO  "assert-deq-member"  (-1)))
    THENA  Auto
    )
  THEN  (All  (RWO  "member\_map"))
  THEN  Auto
  THEN  All  Reduce
  THEN  ExRepD
  THEN  (FLemma  `rcv\_one\_one`  [(-1)])
  THEN  Auto)

---

Home Index