---

Step * 2 of Lemma alpha-equal-varterm


1. opr : Type
2. v : {v:varname()| ¬(v = nullvar() ∈ varname())} 
3. t : term(opr)
4. alpha-eq-terms(opr;varterm(v);t)
5. isvarterm(t) = tt
6. f : opr
7. bts : {bt:bound-term(opr)| bound-term-size(bt) < term-size(t)}  List
8. t = mkterm(f;bts) ∈ term(opr)
⊢ t = varterm(v) ∈ term(opr)
BY
{ ((Assert isvarterm(t) = ff BY (RWO "-1" 0 THEN Auto)) THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  v  :  \{v:varname()|  \mneg{}(v  =  nullvar())\} 
3.  t  :  term(opr)
4.  alpha-eq-terms(opr;varterm(v);t)
5.  isvarterm(t)  =  tt
6.  f  :  opr
7.  bts  :  \{bt:bound-term(opr)|  bound-term-size(bt)  <  term-size(t)\}    List
8.  t  =  mkterm(f;bts)
\mvdash{}  t  =  varterm(v)


By

---

Latex:
((Assert  isvarterm(t)  =  ff  BY  (RWO  "-1"  0  THEN  Auto))  THEN  Auto)

---

Home Index