---

Step * of Lemma isaxiom-append-nil

∀[l:Base]. (↑isaxiom(l)) supposing ((↑isaxiom(l @ [])) and (l @ [])↓)
BY
{ (Intros
   THEN Try (Complete ((UniverseIsType THEN EqCD THEN CanonicalAuto THEN Auto)))
   THEN All(RepUR ``append list_ind``)
   THEN All(RW UnrollLoopsC)
   THEN AllReduce
   THEN UseWitness ⌜Ax⌝⋅
   THEN HasValueD (-2)
   THEN HVimplies2 (-3) [1]
   THEN HVimplies2 (-4) [1]
   THEN BotDiv) }

---

Latex:

---

Latex:
\mforall{}[l:Base].  (\muparrow{}isaxiom(l))  supposing  ((\muparrow{}isaxiom(l  @  []))  and  (l  @  [])\mdownarrow{})


By

---

Latex:
(Intros
  THEN  Try  (Complete  ((UniverseIsType  THEN  EqCD  THEN  CanonicalAuto  THEN  Auto)))
  THEN  All(RepUR  ``append  list\_ind``)
  THEN  All(RW  UnrollLoopsC)
  THEN  AllReduce
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  HasValueD  (-2)
  THEN  HVimplies2  (-3)  [1]
  THEN  HVimplies2  (-4)  [1]
  THEN  BotDiv)

---

Home Index