---

Step * 1 1 1 of Lemma rcv_rcv_lemma


1. t' : Top@i
2. l' : Top@i
3. t : Top@i
4. l : Top@i
⊢ (IdLnkDeq l l') ∧b (IdDeq t t') ~ (IdLnkDeq l l') ∧b (IdDeq t t')
BY
{ Try SqEqCD }

---

Latex:



1.  t'  :  Top@i
2.  l'  :  Top@i
3.  t  :  Top@i
4.  l  :  Top@i
\mvdash{}  (IdLnkDeq  l  l')  \mwedge{}\msubb{}  (IdDeq  t  t')  \msim{}  (IdLnkDeq  l  l')  \mwedge{}\msubb{}  (IdDeq  t  t')


By

Try  SqEqCD

---

Home Index