---

Step * 2 2 1 of Lemma term-ext


1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. x1 : {v:varname()| ¬(v = nullvar() ∈ varname())} 
⊢ (coterm-size(inl x1))↓
BY
{ (RepUR ``coterm-size`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  coterm(opr)  \mequiv{}  coterm-fun(opr;coterm(opr))
3.  x1  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
\mvdash{}  (coterm-size(inl  x1))\mdownarrow{}


By

---

Latex:
(RepUR  ``coterm-size``  0  THEN  Auto)

---

Home Index