test-suite/ssr/ipat_apply.v


1
2
3
4
5
6
7
8
9
10
11
12
13

Require Import ssreflect.

Section Apply.

Variable P : nat -> Prop.
Lemma test_apply A B : forall (f : A -> B) (a : A), B.

Proof.
move=> /[apply] b.
exact.
Qed.

End Apply.