---

Step * of Lemma intuitionistic-pigeonhole

∀A,B:ℕ ⟶ ℙ.
  ((∀s:StrictInc. ⇃(∃n:ℕ. A[s n])) ⇒ (∀s:StrictInc. ⇃(∃n:ℕ. B[s n])) ⇒ (∀s:StrictInc. ⇃(∃n:ℕ. (A[s n] ∧ B[s n]))))
BY
{ (Auto THEN (InstLemma `unary-almost-full-has-strict-inc` [⌜λ2n.A[s n]⌝]⋅ THENA Auto)) }

1
1. A : ℕ ⟶ ℙ@i'
2. B : ℕ ⟶ ℙ@i'
3. ∀s:StrictInc. ⇃(∃n:ℕ. A[s n])@i
4. ∀s:StrictInc. ⇃(∃n:ℕ. B[s n])@i
5. s : StrictInc@i
6. s@0 : StrictInc@i
⊢ ⇃(∃n:ℕ. A[s (s@0 n)])

2
1. A : ℕ ⟶ ℙ@i'
2. B : ℕ ⟶ ℙ@i'
3. ∀s:StrictInc. ⇃(∃n:ℕ. A[s n])@i
4. ∀s:StrictInc. ⇃(∃n:ℕ. B[s n])@i
5. s : StrictInc@i
6. ⇃(∃s@0:StrictInc. ∀n:ℕ. A[s (s@0 n)])
⊢ ⇃(∃n:ℕ. (A[s n] ∧ B[s n]))

---

Latex:

---

Latex:
\mforall{}A,B:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}s:StrictInc.  \00D9(\mexists{}n:\mBbbN{}.  A[s  n]))
    {}\mRightarrow{}  (\mforall{}s:StrictInc.  \00D9(\mexists{}n:\mBbbN{}.  B[s  n]))
    {}\mRightarrow{}  (\mforall{}s:StrictInc.  \00D9(\mexists{}n:\mBbbN{}.  (A[s  n]  \mwedge{}  B[s  n]))))


By

---

Latex:
(Auto  THEN  (InstLemma  `unary-almost-full-has-strict-inc`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.A[s  n]\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index