---

Step * of Lemma lnk-decls-compatible

∀[l1,l2:IdLnk]. ∀[d1,d2:tg:Id fp-> Type].  lnk-decl(l1;d1) || lnk-decl(l2;d2) supposing (l1 = l2 ∈ IdLnk) ⇒ d1 || d2
BY
{ (((UnivCD THENA Auto) THEN Decide ⌈l1 = l2 ∈ IdLnk⌉⋅) THENA 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
⊢ lnk-decl(l1;d1) || lnk-decl(l2;d2)

2
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)

---

Latex:


\mforall{}[l1,l2:IdLnk].  \mforall{}[d1,d2:tg:Id  fp->  Type].
    lnk-decl(l1;d1)  ||  lnk-decl(l2;d2)  supposing  (l1  =  l2)  {}\mRightarrow{}  d1  ||  d2


By

(((UnivCD  THENA  Auto)  THEN  Decide  \mkleeneopen{}l1  =  l2\mkleeneclose{}\mcdot{})  THENA  Auto)

---

Home Index