test-suite/bugs/closed/4234.v


1
2
3
4
5
6
7

Definition UU := Type.

Definition dirprodpair {X Y : UU} := existT (fun x : X => Y).

Definition funtoprodtoprod {X Y Z : UU} : { a : X -> Y & X -> Z }.
Proof.
  refine (dirprodpair _ (fun x => _)).