proposition: Lemma prod_rel_eq : forall (A B:Type), (@eq A) ⊗ (@eq B) ≡ @eq (A * B).
proof: Proof. intros. unfold eq_rel; split; unfold subrelationH; intros. - destruct x, y. repeat red in H. destruct H. cbn in *; subst; reflexivity. - destruct x; destruct y. cbn in H. repeat red. inversion H. split; reflexivity. Qed.
imports: Coq(Morphisms Setoid Relation_Definitions RelationClasses ) ITree(Basics.Utils Indexed.Sum)