---

Step * of Lemma strict-strict1

∀F:Base. (strict(F) ⇒ strict1(λx.F[x]))
BY
{ (Auto
   THEN All (RepUR ``strict strict1 so_apply``)
   THEN SplitAndHyps
   THEN SplitAndConcl
   THEN Try (Hypothesis)
   THEN RepeatFor 2 (ParallelLast)
   THEN D 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}F:Base.  (strict(F)  {}\mRightarrow{}  strict1(\mlambda{}x.F[x]))


By

---

Latex:
(Auto
  THEN  All  (RepUR  ``strict  strict1  so\_apply``)
  THEN  SplitAndHyps
  THEN  SplitAndConcl
  THEN  Try  (Hypothesis)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  D  0
  THEN  Auto)

---

Home Index