---

Step * 1 of Lemma lnk-decl-ap


1. x1 : IdLnk
2. x2 : Id
3. l : IdLnk
4. dt : x:Id fp-> Type
5. ↑rcv(x1,x2) ∈ dom(lnk-decl(l;dt))
⊢ lnk-decl(l;dt)(rcv(x1,x2)) ~ dt(x2)
BY
{ ((((FLemma `lnk-decl-dom2`[(-1)]) THENA Auto)
    THEN (HypSubst' (-1) 0)
    THEN (HypSubst' (-1) (-2))
    THEN (DupHyp (-2))
    THEN (RWO "lnk-decl-dom" (-1)))
   THENA Auto
   ) }

1
1. x1 : IdLnk
2. x2 : Id
3. l : IdLnk
4. dt : x:Id fp-> Type
5. ↑rcv(l,x2) ∈ dom(lnk-decl(l;dt))
6. x1 = l ∈ IdLnk
7. ↑x2 ∈ dom(dt)
⊢ lnk-decl(l;dt)(rcv(l,x2)) ~ dt(x2)

---

Latex:



1.  x1  :  IdLnk
2.  x2  :  Id
3.  l  :  IdLnk
4.  dt  :  x:Id  fp->  Type
5.  \muparrow{}rcv(x1,x2)  \mmember{}  dom(lnk-decl(l;dt))
\mvdash{}  lnk-decl(l;dt)(rcv(x1,x2))  \msim{}  dt(x2)


By

((((FLemma  `lnk-decl-dom2`[(-1)])  THENA  Auto)
    THEN  (HypSubst'  (-1)  0)
    THEN  (HypSubst'  (-1)  (-2))
    THEN  (DupHyp  (-2))
    THEN  (RWO  "lnk-decl-dom"  (-1)))
  THENA  Auto
  )

---

Home Index