---

Step * 1 1 2 2 of Lemma cons_sublist_cons


1. [T] : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. f : ℕ||L1|| + 1 ⟶ ℕ||L2|| + 1
7. increasing(f;||L1|| + 1)
8. ∀j:ℕ||L1|| + 1. ([x1 / L1][j] = [x2 / L2][f j] ∈ T)
9. [x1 / L1][0] = [x2 / L2][f 0] ∈ T
10. f 0 ≠ 0
⊢ increasing(λj.((f j) - 1);||L1|| + 1)
BY
{ (((Unfold `increasing` 0 THEN Reduce 0) THEN Auto)
   THEN AllHyps (\j. ((Unfold `increasing` j THEN InstHyp [i] j) THEN Auto))
   ) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x1  :  T
3.  x2  :  T
4.  L1  :  T  List
5.  L2  :  T  List
6.  f  :  \mBbbN{}||L1||  +  1  {}\mrightarrow{}  \mBbbN{}||L2||  +  1
7.  increasing(f;||L1||  +  1)
8.  \mforall{}j:\mBbbN{}||L1||  +  1.  ([x1  /  L1][j]  =  [x2  /  L2][f  j])
9.  [x1  /  L1][0]  =  [x2  /  L2][f  0]
10.  f  0  \mneq{}  0
\mvdash{}  increasing(\mlambda{}j.((f  j)  -  1);||L1||  +  1)


By

---

Latex:
(((Unfold  `increasing`  0  THEN  Reduce  0)  THEN  Auto)
  THEN  AllHyps  (\mbackslash{}j.  ((Unfold  `increasing`  j  THEN  InstHyp  [i]  j)  THEN  Auto))
  )

---

Home Index