simp only [instBot, evaluate, not_false_eq_true, implies_true]
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom
no goals