aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/5501.v
blob: 24739a3658ff855d5831ed3826f66b29daa39bed (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
Set Universe Polymorphism.

Record Pred@{A} :=
  { car :> Type@{A}
  ; P : car -> Prop
  }.

Class All@{A} (A : Pred@{A}) : Type :=
  { proof : forall (a : A), P A a
  }.

Record Pred_All@{A} : Type :=
  { P' :> Pred@{A}
  ; P'_All : All P'
  }.

Global Instance Pred_All_instance (A : Pred_All) : All A := P'_All A.

Definition Pred_All_proof {A : Pred_All} (a : A) : P A a.
Proof.
solve[auto using proof].