---

Step * 1 1 1 1 2 2 1 1 of Lemma generic-non-empty


1. T : Type
2. X : T
3. R : ℕ ⟶ (T List) ⟶ ℙ
4. p : i:ℕ ⟶ s:(T List) ⟶ (∃s':T List. (s ≤ s' ∧ (R i s')))
5. i : ℤ
6. ||fst((p 0 []))|| ≤ 0
7. s' : T List
8. v2 : [X] ≤ s'
9. v3 : R 0 s'
10. (p 0 [X]) = <s', v2, v3> ∈ (∃s':T List. ([X] ≤ s' ∧ (R 0 s')))
⊢ 0 < ||s'||
BY
{ (((FLemma `iseg_length` [(-3)]) THENA Auto) THEN (Reduce (-1)) THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  X  :  T
3.  R  :  \mBbbN{}  {}\mrightarrow{}  (T  List)  {}\mrightarrow{}  \mBbbP{}
4.  p  :  i:\mBbbN{}  {}\mrightarrow{}  s:(T  List)  {}\mrightarrow{}  (\mexists{}s':T  List.  (s  \mleq{}  s'  \mwedge{}  (R  i  s')))
5.  i  :  \mBbbZ{}
6.  ||fst((p  0  []))||  \mleq{}  0
7.  s'  :  T  List
8.  v2  :  [X]  \mleq{}  s'
9.  v3  :  R  0  s'
10.  (p  0  [X])  =  <s',  v2,  v3>
\mvdash{}  0  <  ||s'||


By

---

Latex:
(((FLemma  `iseg\_length`  [(-3)])  THENA  Auto)  THEN  (Reduce  (-1))  THEN  Auto')

---

Home Index