Theorem: cong (Test/Bool/Cong.lean)

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