Statement

Proof

Symbols

\forall ∀ · \exists ∃ · \in ∈ · \notin ∉ · \empty ∅
\to → · \iff ↔ · \and ∧ · \or ∨ · \not ¬
\powerset 𝒫 · \cup ∪ · \cap ∩ · \setminus ∖ · \subset ⊆ · \omega ω
\mapsto ↦ · \ne ≠ · \bot ⊥ · \preceq ≼ · \simeq ≃
\< ⟨ · \> ⟩ for patterns. Type a command, then Space, Tab, or Enter.

Check runs the kernel on your proof; Hint shows the next step when you are stuck.

Goal

Press Check to see the current goal.