---

Step * 1 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
{ ((HypSubst' (-1) 0) THEN ThinTrivial THEN 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
6. d1 || d2
7. x : Knd@i
8. ↑x ∈ dom(lnk-decl(l2;d1))@i
9. ↑x ∈ dom(lnk-decl(l2;d2))@i
⊢ lnk-decl(l2;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.  l1  =  l2
\mvdash{}  lnk-decl(l1;d1)  ||  lnk-decl(l2;d2)


By

((HypSubst'  (-1)  0)  THEN  ThinTrivial  THEN  Unfold  `fpf-compatible`  0  THEN  Auto)\mcdot{}

---

Home Index