---

Step * of Lemma almost_full0

∀[T:Type]. ∀[R:0-aryRel(T)].  ((R (λi.⊥)) ⇒ almost_full(T;0;R))
BY
{ (Auto THEN (D 0 THEN Auto) THEN With ⌜λi.⊥⌝ (D 0)⋅ THEN Auto THEN EAuto 1) }

1
1. [T] : Type
2. [R] : 0-aryRel(T)
3. R (λi.⊥)
4. f : ℕ ⟶ T
5. strictly-increasing-seq(0;λi.⊥)
⊢ R (f o (λi.⊥))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:0-aryRel(T)].    ((R  (\mlambda{}i.\mbot{}))  {}\mRightarrow{}  almost\_full(T;0;R))


By

---

Latex:
(Auto  THEN  (D  0  THEN  Auto)  THEN  With  \mkleeneopen{}\mlambda{}i.\mbot{}\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  EAuto  1)

---

Home Index