proposition: Lemma option_rel_eq : forall {A : Type}, eq_rel (@eq (option A)) (option_rel eq).
proof: Proof. intros ?; split; intros [] [] EQ; subst; try inv EQ; cbn; auto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)