test-suite/bugs/closed/7854.v


1
2
3
4
5
6
7
8
9
10

Set Primitive Projections.

CoInductive stream (A : Type) := cons {
  hd : A;
  tl : stream A;
}.

CoFixpoint const {A} (x : A) := cons A x (const x).

Check (@eq_refl _ (const tt) <<: tl unit (const tt) = const tt).