proposition: Theorem appendfAppend : forall L1 L2 : list A, append L1 L2 (appendf L1 L2).
proof: Proof. intros L1; elim L1; simpl in |- *. intros L2; case L2; simpl in |- *; auto with datatypes core. intros a l H' L2; case L2; simpl in |- *; auto with datatypes core. intros a0 l0. case (ltADec a a0); intros s; auto. Casec s; intros s; auto. apply appendLtA2; auto. elim l0; auto. intros a1 l1 H'0. case (ltADec a a1); intros s1; auto. Casec s1; intros s1; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)