---

Step * 1 of Lemma l-first-when-none


1. T : Type
2. f : T ⟶ 𝔹
3. u : T
4. v : T List
5. rec-case(v) of [] => inr (λx.Ax)  | x::xs => r.if f[x] then inl x else r fi  ~ inr (λx.Ax)  supposing (∀x∈v.¬↑f[x])
6. ↑f[u]
7. (∀x∈[u / v].¬↑f[x])
⊢ inl u ~ inr (λx.Ax) 
BY
{ (With ⌜0⌝ (D (-1))⋅ THENA Auto) }

1
1. T : Type
2. f : T ⟶ 𝔹
3. u : T
4. v : T List
5. rec-case(v) of [] => inr (λx.Ax)  | x::xs => r.if f[x] then inl x else r fi  ~ inr (λx.Ax)  supposing (∀x∈v.¬↑f[x])
6. ↑f[u]
7. ¬↑f[[u / v][0]]
⊢ inl u ~ inr (λx.Ax) 

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  rec-case(v)  of
      []  =>  inr  (\mlambda{}x.Ax) 
      x::xs  =>
        r.if  f[x]  then  inl  x  else  r  fi    \msim{}  inr  (\mlambda{}x.Ax)   
      supposing  (\mforall{}x\mmember{}v.\mneg{}\muparrow{}f[x])
6.  \muparrow{}f[u]
7.  (\mforall{}x\mmember{}[u  /  v].\mneg{}\muparrow{}f[x])
\mvdash{}  inl  u  \msim{}  inr  (\mlambda{}x.Ax) 


By

---

Latex:
(With  \mkleeneopen{}0\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)

---

Home Index