blob: 2c8b099ef05ed7c815155a3bfdebe6b31d7d45f8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Fixpoint iter {A} (n : nat) (f : A -> A) (x : A) :=
match n with
| 0 => x
| S n => iter n f (f x)
end.
Goal nat -> True.
Proof.
intros n.
evar (f : nat -> nat).
cut (iter 10 f 0 = 0).
vm_compute.
intros; constructor.
instantiate (f := (fun x => x)).
reflexivity.
Qed.
Goal exists x, x = 5 + 5.
Proof.
eexists.
vm_compute.
reflexivity.
Qed.
|
