---

Step * 1 1 of Lemma sublist_pair


1. [T] : Type
2. L : T List
3. i : ℕ||L||
4. j : ℕ||L||
5. i < j
⊢ increasing(λn.if (n =z 0) then i else j fi ;2)
BY
{ (Unfold `increasing` 0 THEN Reduce 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  i  :  \mBbbN{}||L||
4.  j  :  \mBbbN{}||L||
5.  i  <  j
\mvdash{}  increasing(\mlambda{}n.if  (n  =\msubz{}  0)  then  i  else  j  fi  ;2)


By

---

Latex:
(Unfold  `increasing`  0  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index