proposition: Lemma Sorted_fmap (R1 : relation A) (R2 : relation B) l : (∀ x y, R1 x y → R2 (f x) (f y)) → Sorted R1 l → Sorted R2 (f <$> l).
proof: Proof. induction 2; simpl; constructor; eauto using HdRel_fmap. Qed.
imports: stdpp(options)