---

Step * 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') ~ l = l' ∧b t = t'
BY
{ Try (RW (AddrC [2] (RepeatC (UnfoldsC ``eq_lnk eq_id eqof``))) 0)⋅ }

1
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')

---

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{}  l  =  l'  \mwedge{}\msubb{}  t  =  t'


By

Try  (RW  (AddrC  [2]  (RepeatC  (UnfoldsC  ``eq\_lnk  eq\_id  eqof``)))  0)\mcdot{}

---

Home Index