blob: bf86f5117e28463717e222361448b217bc645605 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Class Bin {P:Type} (A B : P) := {}.
Set Primitive Projections.
Record test (n : nat) := { proj : Prop }.
Axiom Bin_test : forall {t1 t2 : test O}, Bin (proj _ t1) (proj _ t2).
Create HintDb db discriminated.
#[local] Hint Resolve Bin_test : db.
#[local] Hint Opaque proj : db.
Goal forall t1 t2 : test O, Bin (proj O t1) (proj O t2).
Proof.
intros.
solve [typeclasses eauto with db].
Qed.
|
