blob: cc11aa93b63a6deeba10c6f7fbdc30a49cfb12c2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Axiom X : Type.
Axiom P : (X -> unit) -> Prop.
Axiom F: unit -> unit.
Axiom G : unit -> unit.
Lemma Hyp ss':
P (fun y : X => ss') ->
P (fun y : X => G (F ss')).
Admitted.
Lemma bug : exists x, P x.
Proof.
intros.
eexists (fun y : X => G _).
eapply Hyp. cbn beta.
Abort.
|
