proposition: Theorem iso_from_x : forall (x : B), to (from x) = x.
proof: Proof. intros. destruct H. simpl. rewrite <- uncompose with (f := to0). rewrite iso_from0. reflexivity. assumption. Qed.
imports: Ssreflect.choice Basics Endo FCompose Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Relations.Relation_Definitions