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