∀[g,h:GrpSig]. ∀[f:MonHom(g,h)].  ((f e) = e ∈ |h|){ ((UnivCD) THENA Auto) }1. g : GrpSig2. h : GrpSig3. f : MonHom(g,h)⊢ (f e) = e ∈ |h|