blob: 102a2aba0d19d12c35700ab06927ab0b3587bb1f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
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.
|
