Theorem: LoVe.BackwardProofs.fst_of_two_props_exact (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

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