Theorem: L2 (LeanTeaching/Ex2/1.lean)

State before:
P Q : Prop
h : ¬Q ↔ P
⊢ (¬P → Q) ∧ (P → ¬Q)
Tactic:
sorry
State after:
no goals