1 2 3 4 5 6 7
Goal forall A B, A * B -> A. Proof. intros A B H. match goal with | [ H : _ * _ |- _ ] => exact (fst H) end. Qed.