---

Step * 1 1 1 1 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. 1 ≤ ((i + 1) + 1)
7. ||fst((p (i + 1) primrec(i + 1;[];λi,s. if i <z ||fst((p i s))|| then fst((p i s)) else fst((p i (s @ [X]))) fi )))||\000C 
   ≤ (i + 1)
8. v : T List
9. primrec(i + 1;[];λi,s. if i <z ||fst((p i s))|| then fst((p i s)) else fst((p i (s @ [X]))) fi ) = v ∈ (T List)
10. s' : T List
11. v3 : v @ [X] ≤ s'
12. v4 : R (i + 1) s'
13. (p (i + 1) (v @ [X])) = <s', v3, v4> ∈ (∃s':T List. (v @ [X] ≤ s' ∧ (R (i + 1) s')))
⊢ v ≤ s'
BY
{ ((Using [`l2',⌜v @ [X]⌝] (BLemma `iseg_transitivity`))⋅
   THEN Auto
   THEN BLemma `iseg_append`
   THEN Auto
   THEN BLemma `iseg_weakening`
   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  :  \mBbbN{}
6.  1  \mleq{}  ((i  +  1)  +  1)
7.  ||fst((p  (i  +  1) 
                    primrec(i  +  1;[];\mlambda{}i,s.  if  i  <z  ||fst((p  i  s))||
                                                                then  fst((p  i  s))
                                                                else  fst((p  i  (s  @  [X])))
                                                                fi  )))||  \mleq{}  (i  +  1)
8.  v  :  T  List
9.  primrec(i  +  1;[];\mlambda{}i,s.  if  i  <z  ||fst((p  i  s))||  then  fst((p  i  s))  else  fst((p  i  (s  @  [X])))  fi  )  \000C=  v
10.  s'  :  T  List
11.  v3  :  v  @  [X]  \mleq{}  s'
12.  v4  :  R  (i  +  1)  s'
13.  (p  (i  +  1)  (v  @  [X]))  =  <s',  v3,  v4>
\mvdash{}  v  \mleq{}  s'


By

---

Latex:
((Using  [`l2',\mkleeneopen{}v  @  [X]\mkleeneclose{}]  (BLemma  `iseg\_transitivity`))\mcdot{}
  THEN  Auto
  THEN  BLemma  `iseg\_append`
  THEN  Auto
  THEN  BLemma  `iseg\_weakening`
  THEN  Auto)\mcdot{}

---

Home Index