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