blob: e5e8a89278d80b371b53f1926a04cdf9d2b9de78 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
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].
Abort.
|
