---

Step * of Lemma sq_stable__is_accum_splitting

∀[T,A:Type]. ∀[L:T List]. ∀[LL:(T List × A) List]. ∀[L2:T List × A]. ∀[f:(T List × A) ⟶ 𝔹]. ∀[x:A].
∀[g:(T List × A) ⟶ A].
  SqStable(is_accum_splitting(T;A;L;LL;L2;f;g;x))
BY
{ (xxxAutoxxx THEN RepUR ``is_accum_splitting l_all`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[L:T  List].  \mforall{}[LL:(T  List  \mtimes{}  A)  List].  \mforall{}[L2:T  List  \mtimes{}  A].  \mforall{}[f:(T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:A].
\mforall{}[g:(T  List  \mtimes{}  A)  {}\mrightarrow{}  A].
    SqStable(is\_accum\_splitting(T;A;L;LL;L2;f;g;x))


By

---

Latex:
(xxxAutoxxx  THEN  RepUR  ``is\_accum\_splitting  l\_all``  0  THEN  Auto)

---

Home Index