test-suite/bugs/opened/4813.v


1
2
3
4
5

Require Import Program.Tactics.

Record T := BT { t : Set }.
Record U (x : T) := BU { u : t x -> Prop }.
Program Definition A (H : unit -> Prop) : U (BT unit) := BU _ H.