---

Step * of Lemma l-first-when-none

∀[T:Type]. ∀[f:T ⟶ 𝔹]. ∀[L:T List].  l-first(x.f[x];L) ~ inr (λx.Ax)  supposing (∀x∈L.¬↑f[x])
BY
{ (Unfold `l-first` 0
   THEN InductionOnList
   THEN Reduce 0
   THEN ((BoolCase ⌜f[u]⌝⋅ THENA Auto) ORELSE Auto')
   THEN ((DoSubsume THENL [Hypothesis; Auto]) ORELSE 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. (∀x∈[u / v].¬↑f[x])
⊢ inl u ~ inr (λx.Ax) 

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].    l-first(x.f[x];L)  \msim{}  inr  (\mlambda{}x.Ax)    supposing  (\mforall{}x\mmember{}L.\mneg{}\muparrow{}f[x])


By

---

Latex:
(Unfold  `l-first`  0
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  ((BoolCase  \mkleeneopen{}f[u]\mkleeneclose{}\mcdot{}  THENA  Auto)  ORELSE  Auto')
  THEN  ((DoSubsume  THENL  [Hypothesis;  Auto])  ORELSE  Auto))

---

Home Index