Theorem: LoVe.BackwardProofs.K (LoVe/Labs/Lab2Solution.lean)

State before:
a b : Prop
⊢ a → b → b
Tactic:
intro ha hb
State after:
a b : Prop
ha : a
hb : b
⊢ b

State before:
a b : Prop
ha : a
hb : b
⊢ b
Tactic:
exact hb
State after:
no goals