proposition: Lemma Sorted_StronglySorted : Transitive R -> forall l, Sorted l -> StronglySorted l.
proof: Proof. induction 2; constructor; trivial. apply Sorted_extends; trivial. constructor; trivial. Qed.
imports: List Relations Relations_1