Library Function_bug

Require Import types.
Require Import Recdef.

Inductive array (A:Type):nat->Type:=
|nil : array A 0
|cons : forall n:nat, A -> array A n -> array A (S n).

Implicit Arguments cons [A n].
Infix "::" := cons (at level 60, right associativity).

Lemma array_typeequality_up: forall (A:Type) (m n:nat),
m=n->array A m=array A n.

Qed.