proposition: Lemma StronglySorted_Sorted : forall l, StronglySorted l -> Sorted l.
proof: Proof. induction 1 as [|? ? ? ? HForall]; constructor; trivial. destruct HForall; constructor; trivial. Qed.
imports: List Relations Relations_1