blob: 7b0883f910fd3b6a53e5d9e46dcb3ba2e5c7a2f6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Require Import RelationClasses.
Axiom R : Prop -> Prop -> Prop.
Declare Instance : Reflexive R.
Class bar := { x : False }.
Record foo := { a : Prop ; b : bar }.
Definition default_foo (a0 : Prop) `{b : bar} : foo := {| a := a0 ; b := b |}.
Goal exists k, R k True.
Proof.
eexists.
evar (b : bar).
let e := match goal with |- R ?e _ => constr:(e) end in
unify e (a (default_foo True)).
subst b.
reflexivity.
Abort.
|
