Step
*
1
1
of Lemma
lnk-decl-ap
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)
BY
{ (((InstLemma `lnk-decl-cap` [⌈l⌉; ⌈dt⌉; ⌈x2⌉; ⌈Void⌉])⋅ THENA Auto)
THEN (NthHypSq (-1))
THEN EqCD
THEN Unfold `fpf-cap` 0
THEN SplitOnConclITE
THEN Auto) }
Latex:
1. x1 : IdLnk
2. x2 : Id
3. l : IdLnk
4. dt : x:Id fp-> Type
5. \muparrow{}rcv(l,x2) \mmember{} dom(lnk-decl(l;dt))
6. x1 = l
7. \muparrow{}x2 \mmember{} dom(dt)
\mvdash{} lnk-decl(l;dt)(rcv(l,x2)) \msim{} dt(x2)
By
(((InstLemma `lnk-decl-cap` [\mkleeneopen{}l\mkleeneclose{}; \mkleeneopen{}dt\mkleeneclose{}; \mkleeneopen{}x2\mkleeneclose{}; \mkleeneopen{}Void\mkleeneclose{}])\mcdot{} THENA Auto)
THEN (NthHypSq (-1))
THEN EqCD
THEN Unfold `fpf-cap` 0
THEN SplitOnConclITE
THEN Auto)
Home
Index