blob: 439782c9e5cbc99cbe58e2cf7f3a1e76bac04e59 (
plain)
1
2
3
4
5
6
7
8
9
|
Class C (A : Type) := c : A -> Type.
Record Inhab (A : Type) := { witness : A }.
Instance inhab_C : C Type := Inhab.
Variable full : forall A (X : C A), forall x : A, c x.
Definition truc {A : Type} : Inhab A := (full _ _ _).
|