---

Step * 2 of Lemma basic_strong_bar_induction


1. T : Type
2. R : n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ
3. B : n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ
4. A : n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ
5. ∀n:ℕ. ∀s:R-consistent-seq(n).  Dec(B[n;s])
6. ∀n:ℕ. ∀s:R-consistent-seq(n).  (B[n;s] ⇒ A[n;s])
⊢ istype(∀n:ℕ. ∀s:R-consistent-seq(n).  ((∀t:{t:T| R n s t} . A[n + 1;s.t@n]) ⇒ A[n;s]))
BY
{ (At ⌜Type⌝ UniverseIsType⋅ THEN EqCD THEN Auto THEN D -2 THEN MemTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  B  :  n:\mBbbN{}  {}\mrightarrow{}  R-consistent-seq(n)  {}\mrightarrow{}  \mBbbP{}
4.  A  :  n:\mBbbN{}  {}\mrightarrow{}  R-consistent-seq(n)  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    Dec(B[n;s])
6.  \mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    (B[n;s]  {}\mRightarrow{}  A[n;s])
\mvdash{}  istype(\mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    ((\mforall{}t:\{t:T|  R  n  s  t\}  .  A[n  +  1;s.t@n])  {}\mRightarrow{}  A[n;s]))


By

---

Latex:
(At  \mkleeneopen{}Type\mkleeneclose{}  UniverseIsType\mcdot{}  THEN  EqCD  THEN  Auto  THEN  D  -2  THEN  MemTypeCD  THEN  Auto)

---

Home Index