proposition: Lemma eq_id_l: forall {A B} (R : relationH A B), R ∘ (@eq A) ≡ R.
proof: Proof. split; intros!. - cbn in *. destruct H as (b & EQ & HR). rewrite EQ. assumption. - cbn. exists x. split; auto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)