proposition: Theorem iso_prop_x : forall {X} (a : X -> A) (b : X -> B), (forall (x : X), a x = from (b x)) <-> (forall (x : X), to (a x) = b x).
proof: Proof. intros. destruct H; simpl. assert (forall x, to0 (a x) = (to0 ∘ a) x). auto. assert (forall x, from0 (b x) = (from0 ∘ b) x). auto. split; intros; [ specialize (H0 x); rewrite H0 | specialize (H1 x); rewrite H1; symmetry ]; apply equal_f; rewrite <- comp_id_left; [ rewrite <- iso_from0 | rewrite <- iso_to0 ]; rewrite <- comp_assoc; extensionality y; unfold compose; rewrite <- H2; auto. Qed.
imports: Ssreflect.choice Basics Endo FCompose Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Relations.Relation_Definitions