blob: 13944770279f65fb49eae441e16b36dfb4b9807c (
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 _ _ _).
|