proposition: Theorem iso_prop : forall {X} (a : X -> A) (b : X -> B), a = from ∘ b <-> to ∘ a = b.
proof: Proof. intros. destruct H. simpl. split; intros. rewrite <- comp_id_left. rewrite <- iso_from0. rewrite <- comp_assoc. rewrite <- H0. reflexivity. symmetry. rewrite <- comp_id_left. rewrite <- iso_to0. rewrite <- comp_assoc. rewrite <- H0. reflexivity. Qed.
imports: Ssreflect.choice Basics Endo FCompose Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Relations.Relation_Definitions