---

Step * 1 of Lemma firstn_append


∀[L2:Top List]. ∀[n:ℕ1].  (case L2 of [] => [] | a::as' => if 0 <z n then [a / firstn(n - 1;as')] else [] fi  esac ~ [])
BY
{ (Auto THEN (D (-2)) THEN Reduce 0 THEN Try (Trivial) THEN SplitOnConclITE THEN Auto') }

---

Latex:

---

Latex:

\mforall{}[L2:Top  List].  \mforall{}[n:\mBbbN{}1].
    (case  L2  of  []  =>  []  |  a::as'  =>  if  0  <z  n  then  [a  /  firstn(n  -  1;as')]  else  []  fi    esac  \msim{}  [])


By

---

Latex:
(Auto  THEN  (D  (-2))  THEN  Reduce  0  THEN  Try  (Trivial)  THEN  SplitOnConclITE  THEN  Auto')

---

Home Index