---

Step * 1 of Lemma first-success-is-inl


1. T : Type
2. A : T ⟶ Type
3. f : x:T ⟶ (A[x]?)
⊢ ∀[j:ℕ0]. ∀[a:A[⊥]].
    ((inr ⋅ ) = (inl <j, a>) ∈ (i:ℕ0 × A[⊥]?) ⇐⇒ j < 0 ∧ ((f ⊥) = (inl a) ∈ (A[⊥]?)) ∧ (∀x∈firstn(j;[]).↑isr(f x)))
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  T  {}\mrightarrow{}  Type
3.  f  :  x:T  {}\mrightarrow{}  (A[x]?)
\mvdash{}  \mforall{}[j:\mBbbN{}0].  \mforall{}[a:A[\mbot{}]].
        ((inr  \mcdot{}  )  =  (inl  <j,  a>)  \mLeftarrow{}{}\mRightarrow{}  j  <  0  \mwedge{}  ((f  \mbot{})  =  (inl  a))  \mwedge{}  (\mforall{}x\mmember{}firstn(j;[]).\muparrow{}isr(f  x)))


By

---

Latex:
TACTIC:Auto

---

Home Index