---

Step * 1 of Lemma general_length_nth_tl


1. r : ℤ
⊢ ∀[L:Top List]. (||L|| = if 0 <z ||L|| then ||L|| - 0 else 0 fi  ∈ ℤ)
BY
{ xxx(Auto THEN SplitOnConclITE THEN Auto')xxx }

---

Latex:

---

Latex:

1.  r  :  \mBbbZ{}
\mvdash{}  \mforall{}[L:Top  List].  (||L||  =  if  0  <z  ||L||  then  ||L||  -  0  else  0  fi  )


By

---

Latex:
xxx(Auto  THEN  SplitOnConclITE  THEN  Auto')xxx

---

Home Index