proposition: Lemma list_ap_app : forall A B (v w: list (A -> B)) x, list_ap (v ++ w) x = list_ap v x ++ list_ap w x.
proof: Proof. induction v; intros; auto. simpl. rewrite IHv. rewrite app_assoc. reflexivity. Qed.
imports: Hask.Ltac Hask.Control.Monad Hask.Data.Eq Hask.Data.Maybe Coq.Program.Wf Coq.Sorting.Sorted Coq.Classes.RelationClasses Coq.Lists.List FunctionalExtensionality