Theorem implication :
forall A B : Prop,
A ->
(A -> B) ->
B
.
Proving: implication 1 subgoal -------------- (1/1) forall A B : Prop, A -> (A -> B) -> B
Proof.
intros A B.
intros proof_of_A.
intros A_implies_B.
pose (proof_of_B := A_implies_B proof_of_A).
exact proof_of_B.
Qed.