Step
*
of Lemma
fpf_join_cons_lemma
∀v,u,eq:Top. (⊕([u / v]) ~ u ⊕ ⊕(v))
BY
{ (UnivCD THENA Auto) }
1
1. v : Top@i
2. u : Top@i
3. eq : Top@i
⊢ ⊕([u / v]) ~ u ⊕ ⊕(v)
Latex:
\mforall{}v,u,eq:Top. (\moplus{}([u / v]) \msim{} u \moplus{} \moplus{}(v))
By
(UnivCD THENA Auto)
Home
Index