proposition: Lemma StronglySorted_impl : forall (A : Type) (P Q : A -> A -> Prop), (forall a b : A, P a b -> Q a b) -> forall l : list A, StronglySorted P l -> StronglySorted Q l.
proof: Proof. intros. induction l; simpl. constructor. constructor. apply IHl. inversion H0; assumption. inversion H0; subst. apply Forall_impl with (P:=P a). apply H. 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