---

Step * of Lemma hereditarily-varterm

No Annotations
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[v:{v:varname()| ¬(v = nullvar() ∈ varname())} ].
  (hereditarily(opr;s.P[s];varterm(v)) ⇐⇒ P[varterm(v)])
BY
{ (Auto THEN D 0 THEN Auto) }

1
1. [opr] : Type
2. [P] : term(opr) ⟶ ℙ
3. [v] : {v:varname()| ¬(v = nullvar() ∈ varname())} 
4. P[varterm(v)]
5. s : term(opr)
6. s << varterm(v)
⊢ P[s]

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[P:term(opr)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:\{v:varname()|  \mneg{}(v  =  nullvar())\}  ].
    (hereditarily(opr;s.P[s];varterm(v))  \mLeftarrow{}{}\mRightarrow{}  P[varterm(v)])


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index