proposition: Lemma subrelationH_trans {A B: Type} (R S T: relationH A B) `{R ⊑ S} `{S ⊑ T} : R ⊑ T.
proof: Proof. intros!; auto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)