---

Step * of Lemma term-induction1-ext

No Annotations
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ].
  ((∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)])
  ⇒ (∀f:opr. ∀bts:bound-term(opr) List.  ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkterm(f;bts)]))
  ⇒ {∀t:term(opr). P[t]})
BY
{ Extract of Obid: term-induction1
  not unfolding  select
  finishing with (RepUR ``so_apply term-ind`` 0 THEN Auto)
  normalizes to:
  
  λv,m,t. term-ind(x.v[x];f,bts,r.m[f;bts;r];t) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[P:term(opr)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}v:\{v:varname()|  \mneg{}(v  =  nullvar())\}  .  P[varterm(v)])
    {}\mRightarrow{}  (\mforall{}f:opr.  \mforall{}bts:bound-term(opr)  List.    ((\mforall{}i:\mBbbN{}||bts||.  P[snd(bts[i])])  {}\mRightarrow{}  P[mkterm(f;bts)]))
    {}\mRightarrow{}  \{\mforall{}t:term(opr).  P[t]\})


By

---

Latex:
Extract  of  Obid:  term-induction1
not  unfolding    select
finishing  with  (RepUR  ``so\_apply  term-ind``  0  THEN  Auto)
normalizes  to:

\mlambda{}v,m,t.  term-ind(x.v[x];f,bts,r.m[f;bts;r];t)

---

Home Index