---

Step * 2 of Lemma lnk-decls-compatible


1. l1 : IdLnk
2. l2 : IdLnk
3. d1 : tg:Id fp-> Type
4. d2 : tg:Id fp-> Type
5. (l1 = l2 ∈ IdLnk) ⇒ d1 || d2
6. ¬(l1 = l2 ∈ IdLnk)
⊢ lnk-decl(l1;d1) || lnk-decl(l2;d2)
BY
{ (Unfold `fpf-compatible` 0 THEN Auto)⋅ }

1
1. l1 : IdLnk
2. l2 : IdLnk
3. d1 : tg:Id fp-> Type
4. d2 : tg:Id fp-> Type
5. (l1 = l2 ∈ IdLnk) ⇒ d1 || d2
6. ¬(l1 = l2 ∈ IdLnk)
7. x : Knd@i
8. ↑x ∈ dom(lnk-decl(l1;d1))@i
9. ↑x ∈ dom(lnk-decl(l2;d2))@i
⊢ lnk-decl(l1;d1)(x) = lnk-decl(l2;d2)(x) ∈ Type

---

Latex:



1.  l1  :  IdLnk
2.  l2  :  IdLnk
3.  d1  :  tg:Id  fp->  Type
4.  d2  :  tg:Id  fp->  Type
5.  (l1  =  l2)  {}\mRightarrow{}  d1  ||  d2
6.  \mneg{}(l1  =  l2)
\mvdash{}  lnk-decl(l1;d1)  ||  lnk-decl(l2;d2)


By

(Unfold  `fpf-compatible`  0  THEN  Auto)\mcdot{}

---

Home Index