test-suite/bugs/closed/2027.v


1
2
3
4
5
6
7
8
9
10
11


Parameter T : Type -> Type.
Parameter f : forall {A}, T A -> T A.
Parameter P : forall {A}, T A -> Prop.
Axiom f_id : forall {A} (l : T A), f l = l.

Goal forall A (p : T A), P p.
Proof.
  intros.
  rewrite <- f_id.
Admitted.