Say we have a proposition P1 n, and there exists n for which it holds. Furthermore we have a proposition P2, where P1 n implies P2 for any n. How do we prove P2?
Parameter P1 : nat -> Prop.
Axiom some_p1 : exists n, P1 n.
Parameter P2 : Prop.
Axiom p1_implies_p2 : forall n, P1 n -> P2.
Theorem p2 : P2.
I tried
Proof.
eapply p1_implies_p2.
which gives me the goal P1 ?n, but I'm not sure how to proceed from there.
You may eliminate some_p1to get a witness nand a hypothesis Hn.
Theorem p2 : P2.
case some_p1 ; intros n Hn. apply (p1_implies_p2 _ Hn).
Qed.
Just for completeness, if you use the SSReflect proof language, Pierre's proof idea would look like this:
Theorem p2 : P2.
Proof. move: some_p1 => [n p1n]. exact: (p1_implies_p2 p1n). Qed.
Note that providing the second argument p1n to p1_implies_p2 is enough, since the omitted first one, n, can be inferred by Coq.