proposition: Lemma transpose_compose {A B C : Type} (R : relationH A B) (S : relationH B C) : † (S ∘ R) ≡ (†R ∘ †S).
proof: Proof. split; unfold transpose; cbn; intros!; cbn in *. - destruct H as (b & HR & HS). exists b. tauto. - destruct H as (b & HR & HS). exists b. tauto. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)