Step * 1 1 1 of Lemma proddeq_reduce_lemma


1. Top@i
2. Top@i
3. Top@i
4. Top@i
5. Top@i
6. Top@i
⊢ (a u) ∧b (b v) (a u) ∧b (b v)
BY
Try SqEqCD }


Latex:


Latex:

1.  v  :  Top@i
2.  u  :  Top@i
3.  y  :  Top@i
4.  x  :  Top@i
5.  b  :  Top@i
6.  a  :  Top@i
\mvdash{}  (a  x  u)  \mwedge{}\msubb{}  (b  y  v)  \msim{}  (a  x  u)  \mwedge{}\msubb{}  (b  y  v)


By


Latex:
Try  SqEqCD




Home Index