proposition: Theorem iso_prop_set : forall (a : A) (b : B), a = from b <-> to a = b.
proof: Proof. intros. split; intros. rewrite H0. apply iso_from_x. symmetry. rewrite <- H0. apply iso_to_x. Qed.
imports: Ssreflect.choice Basics Endo FCompose Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Relations.Relation_Definitions