---

Step * 1 of Lemma rcv_rcv_lemma


1. t' : Top@i
2. l' : Top@i
3. t : Top@i
4. l : Top@i
⊢ rcv(l,t) = rcv(l',t') ~ l = l' ∧b t = t'
BY
{ Try (RW (AddrC [1] (
RepeatC (UnfoldsC ``proddeq product-deq sumdeq union-deq Kind-deq eq_knd eqof locl rcv`` ANDTHENC ReduceC))) 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') ~ l = l' ∧b t = t'

---

Latex:



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


By

Try  (RW  (AddrC  [1]  (
...))  0)\mcdot{}

---

Home Index