---

Step * 1 of Lemma hereditarily-varterm


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]
BY
{ (InstLemma `subterm-varterm` [⌜opr⌝;⌜s⌝;⌜v⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  [P]  :  term(opr)  {}\mrightarrow{}  \mBbbP{}
3.  [v]  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
4.  P[varterm(v)]
5.  s  :  term(opr)
6.  s  <<  varterm(v)
\mvdash{}  P[s]


By

---

Latex:
(InstLemma  `subterm-varterm`  [\mkleeneopen{}opr\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index