Theorem: toForm_toConsExp_eq (Fine/PropositionalLanguage.lean)

State before:
f : Form
⊢ ConsExp.toForm (Form.toConsExp f) = some f
Tactic:
induction f <;> simp! [*]
State after:
no goals