proposition: Theorem app_length' : forall (X : Type) (lst1 lst2 : list X), length (lst1 ++ lst2) = (length lst1) + (length lst2).
proof: Proof. intros; induction lst1; [idtac | simpl; rewrite IHlst1]; reflexivity. Qed.
imports: Coq(Arith List) LF(IndProp)