{G G' H : Group} (f : G $-> H) (f' : G' $-> H) {x y : G} {x' y' : G'} (p : f x = f' x') (q : f y = f' y') : f (x * y) = f' (x' * y'). Proof. lhs nrapply grp_homo_op. rhs nrapply grp_homo_op. exact (ap011 _ p q). Defined.
Require Import Basics Types HProp HFiber HSet. Require Import Homotopy.IdentitySystems. Require Import (notations) Classes.interfaces.canonical_names. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Int. Require Import Truncations.Core.