blob: c930f24df7081fb0d602c53159678f090ad0a2e4 (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* An occur-check test was done too early *)
Goal forall B C : nat -> nat -> Prop, forall k,
(exists A, (forall k', C A k' -> B A k') -> B A k).
Proof.
intros B C k.
econstructor.
intros X.
apply X. (* used to fail here *)
Abort.
|
