Step
*
of Lemma
bottom_diverge
¬(⊥)↓
BY
{ TACTIC:Refine_bottomDiverges }
Latex:
Latex:
\mneg{}(\mbot{})\mdownarrow{}
By
Latex:
TACTIC:Refine\_bottomDiverges
Home
Index