---

Step * of Lemma sublist_pair

No Annotations
∀[T:Type]. ∀L:T List. ∀i,j:ℕ||L||.  [L[i]; L[j]] ⊆ L supposing i < j
BY
{ ((Auto THEN Unfold `sublist` 0 THEN Reduce 0 THEN InstConcl [λn.if (n =z 0) then i else j fi ]⋅)
   THEN Try (Complete (Auto))
   ) }

1
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)
∧ (∀j@0:ℕ2. ([L[i]; L[j]][j@0] = L[(λn.if (n =z 0) then i else j fi ) j@0] ∈ T))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}i,j:\mBbbN{}||L||.    [L[i];  L[j]]  \msubseteq{}  L  supposing  i  <  j


By

---

Latex:
((Auto  THEN  Unfold  `sublist`  0  THEN  Reduce  0  THEN  InstConcl  [\mlambda{}n.if  (n  =\msubz{}  0)  then  i  else  j  fi  ]\mcdot{})
  THEN  Try  (Complete  (Auto))
  )

---

Home Index