proposition: Theorem fappendfAppend : forall L1 L2 : list A, append L1 (map f L2) (fappendf 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 appendLtA1; auto. apply ltAeqAComp with (a := a) (b := a0); auto. generalize (H' (a0 :: l0)); simpl in |- *; auto. apply appendLtA2; auto. apply ltAeqAComp with (a := a0) (b := a); auto. elim l0; auto. intros a1 l1 H'0. case (ltADec a a1); intros s1; auto. Casec s1; intros s1; auto. simpl in |- *. apply appendLtA1; auto. apply ltAeqAComp with (a := a) (b := a1); auto. generalize (H' (a1 :: l1)); simpl in |- *; auto. simpl in |- *; auto. apply appendLtA2; auto. apply ltAeqAComp with (a := a1) (b := a); auto. simpl in |- *. apply appendEqA; auto. apply eqATrans with a1; auto. apply appendEqA; auto. apply eqATrans with a0; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)