proposition: Lemma subrelationH_refl_eq {A: Type} (R: relationH A A) (H : Reflexive R) : @eq A ⊑ R.
proof: Proof. intros!. rewrite H0. cbn. apply H. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)