proposition: Lemma length_add : forall (A : Type) (l1 l2 : list A) a, length (l1 ++ a :: l2) = S (length (l1 ++ l2)).
proof: Proof. intros A l1 l2 a; rewrite app_length; simpl; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; rewrite app_length; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)