---

Step * of Lemma prior-cases

∀[T:Type]
  ∀f:ℕ ⟶ (T + Top). ∀n:ℕ.
    case prior(n;f)
     of inl(p) =>
     let m,x = p 
     in ((f m) = (inl x) ∈ (T + Top)) ∧ (∀k:{m + 1..n-}. (¬↑isl(f k)))
     | inr(q) =>
     ∀k:ℕn. (¬↑isl(f k))
BY
{ (InductionOnNat
   THEN Try ((Unfold `prior` 0 THEN (RWO "natrec-unroll" 0 THENA Auto) THEN Reduce 0 THEN Complete (Auto))⋅)
   ) }

1
.....upcase..... 
1. [T] : Type
2. f : ℕ ⟶ (T + Top)
3. n : ℤ
4. [%1] : 0 < n
5. case prior(n - 1;f)
 of inl(p) =>
 let m,x = p 
 in ((f m) = (inl x) ∈ (T + Top)) ∧ (∀k:{m + 1..n - 1-}. (¬↑isl(f k)))
 | inr(q) =>
 ∀k:ℕn - 1. (¬↑isl(f k))
⊢ case prior(n;f)
 of inl(p) =>
 let m,x = p 
 in ((f m) = (inl x) ∈ (T + Top)) ∧ (∀k:{m + 1..n-}. (¬↑isl(f k)))
 | inr(q) =>
 ∀k:ℕn. (¬↑isl(f k))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  (T  +  Top).  \mforall{}n:\mBbbN{}.
        case  prior(n;f)
          of  inl(p)  =>
          let  m,x  =  p 
          in  ((f  m)  =  (inl  x))  \mwedge{}  (\mforall{}k:\{m  +  1..n\msupminus{}\}.  (\mneg{}\muparrow{}isl(f  k)))
          |  inr(q)  =>
          \mforall{}k:\mBbbN{}n.  (\mneg{}\muparrow{}isl(f  k))


By

---

Latex:
(InductionOnNat
  THEN  Try  ((Unfold  `prior`  0
                        THEN  (RWO  "natrec-unroll"  0  THENA  Auto)
                        THEN  Reduce  0
                        THEN  Complete  (Auto))\mcdot{})
  )

---

Home Index