proposition: Theorem surjective_pairing_stuck : forall (p : natprod), p = (fst p, snd p).
proof: Proof. simpl. Abort. Theorem surjective_pairing : forall (p : natprod), p = (fst p, snd p). Proof. intros p. destruct p as [n m]. simpl. reflexivity. Qed.