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: Coq.Sorting.Sorted Coq.Sorting.Permutation Category.Lib Category.Theory.Functor Category.Theory.Coq.Functor Category.Theory.Coq.Functor.Proofs Category.Theory.Coq.List Category.Theory.Coq.Maybe