proposition: Lemma map_iso o (x: op_type B o) (xproper: Proper (=) x): map_op ab ba (map_op ba ab x) = x.
proof: Proof. Proof with auto; try reflexivity. induction o; simpl; intros... intros x0 y H0. change (map_op ab ba (map_op ba ab (x (ab (ba x0)))) = x y). transitivity (x (ab (ba x0))). apply IHo, xproper... apply xproper. rewrite iso, H0... Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra