Theorem: prop_ext (Test/Bool/PropExt.lean)

State before:
p q : Bool
⊢ (p = true ↔ q = true) → (p == q) = true
Tactic:
intro ⟨hpq, hqp⟩
State after:
p q : Bool
hpq : p = true → q = true
hqp : q = true → p = true
⊢ (p == q) = true

State before:
p q : Bool
hpq : p = true → q = true
hqp : q = true → p = true
⊢ (p == q) = true
Tactic:
cases p <;> cases q <;> simp_all
State after:
no goals