---

Step * of Lemma fun_exp_compose2

∀[A,B:Type]. ∀[h:A ⟶ A]. ∀[n:ℕ].  (λg.(g o h)^n = (λg.(g o h^n)) ∈ ((A ⟶ B) ⟶ A ⟶ B))
BY
{ ((InductionOnNat THEN (RW funexpC 0⋅ THENA Auto) THEN Try ((CallByValueReduce 0 THEN Auto)))
   THEN Reduce 0
   THEN Try ((AutoSplit THEN HypSubst (-1) 0 THEN Auto))
   THEN All (RepUR ``compose``)⋅
   THEN Repeat ((EqCD THEN Auto THEN RWO "fun_exp_add_apply1 fun_exp_apply_add1" 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[h:A  {}\mrightarrow{}  A].  \mforall{}[n:\mBbbN{}].    (\mlambda{}g.(g  o  h)\^{}n  =  (\mlambda{}g.(g  o  h\^{}n)))


By

---

Latex:
((InductionOnNat  THEN  (RW  funexpC  0\mcdot{}  THENA  Auto)  THEN  Try  ((CallByValueReduce  0  THEN  Auto)))
  THEN  Reduce  0
  THEN  Try  ((AutoSplit  THEN  HypSubst  (-1)  0  THEN  Auto))
  THEN  All  (RepUR  ``compose``)\mcdot{}
  THEN  Repeat  ((EqCD  THEN  Auto  THEN  RWO  "fun\_exp\_add\_apply1  fun\_exp\_apply\_add1"  0  THEN  Auto)))

---

Home Index