---

Step * of Lemma iterated-conjugate2

∀[T:Type]. ∀[f,g,h:T ⟶ T].
  (∀[n:ℕ]. (g o (f o h)^n = (g o (f^n o h)) ∈ (T ⟶ T))) supposing 
     ((∀b:T. ((h (g b)) = b ∈ T)) and 
     (∀a:T. ((g (h a)) = a ∈ T)))
BY
{ TACTIC:(PrimrecInductionOn `n' THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f,g,h:T  {}\mrightarrow{}  T].
    (\mforall{}[n:\mBbbN{}].  (g  o  (f  o  h)\^{}n  =  (g  o  (f\^{}n  o  h))))  supposing 
          ((\mforall{}b:T.  ((h  (g  b))  =  b))  and 
          (\mforall{}a:T.  ((g  (h  a))  =  a)))


By

---

Latex:
TACTIC:(PrimrecInductionOn  `n'  THEN  Auto)

---

Home Index