---

Step * 1 of Lemma lnk-decl-dom-implies


1. x1 : IdLnk
2. x2 : Id
3. l : IdLnk
4. dt : x:Id fp-> Type
5. ↑rcv(x1,x2) ∈ dom(lnk-decl(l;dt))
⊢ True c∧ (↑x2 ∈ dom(dt))
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))
   THEN Auto) }

---

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{}  True  c\mwedge{}  (\muparrow{}x2  \mmember{}  dom(dt))


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))
  THEN  Auto)

---

Home Index