Step
*
of Lemma
id-is-monoid_hom
∀[A:GrpSig]. (λx.x ∈ MonHom(A,A))
BY
{ (((Unfold `monoid_hom` 0) THEN Auto) THEN MemTypeCD THEN Auto) }
1
.....set predicate.....
1. A : GrpSig
⊢ IsMonHom{A,A}(λx.x)
Latex:
Latex:
\mforall{}[A:GrpSig]. (\mlambda{}x.x \mmember{} MonHom(A,A))
By
Latex:
(((Unfold `monoid\_hom` 0) THEN Auto) THEN MemTypeCD THEN Auto)
Home
Index