---

Step * of Lemma pi-level-pi-replace

∀[t,x:Name]. ∀[P:pi_term()].  (pi-level(pi-replace(t;x;P)) = pi-level(P) ∈ ℤ)
BY
{ (Auto
   THEN (MoveToConcl (-1) THEN BLemma `pi_term-induction` )
   THEN Auto
   THEN (RepUR ``pi-replace pi-level`` 0 THEN Reduce 0 THEN Try (Folds ``pi-level pi-replace`` 0) THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[t,x:Name].  \mforall{}[P:pi\_term()].    (pi-level(pi-replace(t;x;P))  =  pi-level(P))


By

---

Latex:
(Auto
  THEN  (MoveToConcl  (-1)  THEN  BLemma  `pi\_term-induction`  )
  THEN  Auto
  THEN  (RepUR  ``pi-replace  pi-level``  0
              THEN  Reduce  0
              THEN  Try  (Folds  ``pi-level  pi-replace``  0)
              THEN  Auto)\mcdot{})

---

Home Index