---

Step * of Lemma State1-state-class1

∀[Info,B,A:Type]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[init:Id ─→ B]. ∀[X:EClass(A)].
  (State1(init;f;X) = state-class1(init;f;X) ∈ EClass(B))
BY
{ (Auto THEN Unfolds ``State1 state-class1`` 0 THEN BLemma `State-loc-comb-is-loop-class-state` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B,A:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[init:Id  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].
    (State1(init;f;X)  =  state-class1(init;f;X))


By

---

Latex:
(Auto
  THEN  Unfolds  ``State1  state-class1``  0
  THEN  BLemma  `State-loc-comb-is-loop-class-state`
  THEN  Auto)

---

Home Index