proposition: Lemma length_S : forall (A : Set) (l : list A) (n : nat), length A l = S n -> exists h : A, (exists t : list A, l = Cons A h t /\ length A t = n).
proof: Proof. intros A l. case l. simpl in |- *. intros. discriminate H. simpl in |- *. intros h0 t0 n H. injection H. intro. split with h0. split with t0. split. reflexivity. assumption. Qed.
imports: Arith ZArith EqNat dec natZ