---

Step * of Lemma finite-double-negation-shift2

No Annotations
∀[A:ℙ]. ∀n:ℕ. ∀[B:ℕn ⟶ ℙ]. ((∀i:ℕn. (((B i) ⇒ A) ⇒ A)) ⇒ ((∀i:ℕn. (B i)) ⇒ A) ⇒ A)
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN GeneralNatInd (-1) THEN Auto THEN CaseNat 0 `n') }

1
1. [A] : ℙ
2. n : ℕ
3. ∀n1:ℕn. ∀[B:ℕn1 ⟶ ℙ]. ((∀i:ℕn1. (((B i) ⇒ A) ⇒ A)) ⇒ ((∀i:ℕn1. (B i)) ⇒ A) ⇒ A)
4. [B] : ℕn ⟶ ℙ
5. ∀i:ℕn. (((B i) ⇒ A) ⇒ A)
6. (∀i:ℕn. (B i)) ⇒ A
7. n = 0 ∈ ℤ
⊢ A

2
1. [A] : ℙ
2. n : ℕ
3. ∀n1:ℕn. ∀[B:ℕn1 ⟶ ℙ]. ((∀i:ℕn1. (((B i) ⇒ A) ⇒ A)) ⇒ ((∀i:ℕn1. (B i)) ⇒ A) ⇒ A)
4. [B] : ℕn ⟶ ℙ
5. ∀i:ℕn. (((B i) ⇒ A) ⇒ A)
6. (∀i:ℕn. (B i)) ⇒ A
7. ¬(n = 0 ∈ ℤ)
⊢ A

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:\mBbbP{}].  \mforall{}n:\mBbbN{}.  \mforall{}[B:\mBbbN{}n  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}i:\mBbbN{}n.  (((B  i)  {}\mRightarrow{}  A)  {}\mRightarrow{}  A))  {}\mRightarrow{}  ((\mforall{}i:\mBbbN{}n.  (B  i))  {}\mRightarrow{}  A)  {}\mRightarrow{}  A)


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  GeneralNatInd  (-1)  THEN  Auto  THEN  CaseNat  0  `n')

---

Home Index