blob: c875051bdc4efbde21f69b687e23dc86bd3ac3f5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *)
(* tests of Show output with -emacs flag to coqtop; see bug 5535 *)
Theorem nums : forall (n m : nat), n = m -> (S n) = (S m).
Proof.
intros.
induction n as [| n'].
induction m as [| m'].
Show.
Admitted.
|
