proposition: Lemma Forall_insert : forall a (R : a -> a -> Prop) (Q : a -> a -> bool) x xs y, Q x y = true -> (forall a b, R a b <-> Q a b = true) -> List.Forall (R x) xs -> List.Forall (R x) (insert Q y xs).
proof: Proof. intros. apply Permutation_Forall with (xs:=y :: xs). symmetry. apply Permutation_insert. reflexivity. constructor; trivial. apply H0. assumption. 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 Coq.Relations.Relations Coq.Reals.ROrderedType Coq.Lists.List Coq.Sorting.Sorted Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.RelationClasses FunctionalExtensionality