Lemma isunitisob {X Y : setwithbinop} (f : binopiso X Y) (uny : Y) (is : isunit (@op Y) uny) : isunit (@op X) ((invmap f) uny). Proof. set (int := isunitisof (invbinopiso f)). simpl. simpl in int. apply int. apply is. Qed.