Step * of Lemma oal_merge_right_nil_lemma

ps,p,b,a:Top.  ([p ps] ++ [] [p ps])
BY
(UnivCD THENA Auto) }

1
1. ps Top@i
2. Top@i
3. Top@i
4. Top@i
⊢ [p ps] ++ [] [p ps]


Latex:


Latex:
\mforall{}ps,p,b,a:Top.    ([p  /  ps]  ++  []  \msim{}  [p  /  ps])


By


Latex:
(UnivCD  THENA  Auto)




Home Index