proposition: Lemma list_length_S : forall A (l : list A) n, length l = S n -> exists x:A, exists l', l = x :: l'.
proof: Proof. induction l as [ | a ]; intros n Hlen; simpl in *; inversion Hlen; exists a; exists l; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv