Theorem: Form.toConsExp_injective (Fine/PropositionalLanguage.lean)

State before:
⊢ Function.Injective toConsExp
Tactic:
intros f1 f2
State after:
f1 f2 : Form
⊢ toConsExp f1 = toConsExp f2 → f1 = f2

State before:
f1 f2 : Form
⊢ toConsExp f1 = toConsExp f2 → f1 = f2
Tactic:
induction f1 generalizing f2 <;> cases f2 <;> simp! <;> aesop
State after:
no goals