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