1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* This needs step by step unfolding *)
11
Fixpoint T (n:nat) : Prop :=
23
(* This needs unification on type *)
25
Goal forall n m : nat, S m = S n :>nat.
29
(* f_equal : forall (A B:Set) (f:A->B) (x y:A), x=y->(f x)=(f y) *)
30
(* and A cannot be deduced from the goal but only from the type of f, x or y *)