Theorem: red (lean/solutions/04_metam.lean)

State before:
hA : 1 = 1
hB : 2 = 2
⊢ 2 = 2
Tactic:
sorry
State after:
no goals