1
(* Exemple soumis par Pierre Corbineau (bug #1671) *)
3
CoInductive hdlist : unit -> Type :=
4
| cons : hdlist tt -> hdlist tt.
6
Variable P : forall bo, hdlist bo -> Prop.
7
Variable all : forall bo l, P bo l.
9
Definition F (l:hdlist tt) : P tt l :=
10
match l in hdlist u return P u l with
11
| cons (cons l') => all tt _