---

Step * of Lemma sq_stable__action_p

∀[A:Type]. ∀[x:A ⟶ A ⟶ A]. ∀[e:A]. ∀[S:Type]. ∀[f:A ⟶ S ⟶ S].  SqStable(IsAction(A;x;e;S;f))
BY
{ ((Unfold `action_p` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[x:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].  \mforall{}[e:A].  \mforall{}[S:Type].  \mforall{}[f:A  {}\mrightarrow{}  S  {}\mrightarrow{}  S].    SqStable(IsAction(A;x;e;S;f))


By

---

Latex:
((Unfold  `action\_p`  0)  THEN  Auto)

---

Home Index