proposition: Lemma fold_right_commutes : forall s1 s2 x, eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
proof: Proof. intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x. - reflexivity. - transitivity (f a (f x (fold_right f i (s1++s2)))); auto. apply Comp; auto. Qed.
imports: List Sorted Setoid Basics Morphisms