proposition: Lemma StronglySorted_fmap (R1 : relation A) (R2 : relation B) l : (∀ x y, R1 x y → R2 (f x) (f y)) → StronglySorted R1 l → StronglySorted R2 (f <$> l).
proof: Proof. induction 2; csimpl; constructor; rewrite ?Forall_fmap; eauto using Forall_impl. Qed.
imports: stdpp(options)