---

Step * of Lemma disj_un_tr_ap_inl_lemma

∀x,i,tr2,tr1:Top.  (tr1 + tr2 i (inl x) ~ λs.(tr1 i x s))
BY
{ (UnivCD THENA Auto) }

1
1. x : Top@i
2. i : Top@i
3. tr2 : Top@i
4. tr1 : Top@i
⊢ tr1 + tr2 i (inl x) ~ λs.(tr1 i x s)

---

Latex:

---

Latex:
\mforall{}x,i,tr2,tr1:Top.    (tr1  +  tr2  i  (inl  x)  \msim{}  \mlambda{}s.(tr1  i  x  s))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index