---

Step * of Lemma alpha-equal-varterm

No Annotations
∀[opr:Type]. ∀[v:{v:varname()| ¬(v = nullvar() ∈ varname())} ]. ∀[t:term(opr)].
  t = varterm(v) ∈ term(opr) supposing alpha-eq-terms(opr;varterm(v);t)
BY
{ ((Auto
    THEN (Assert isvarterm(t) = tt BY
                ((FLemma `isvarterm_functionality` [-1] THENA Auto) THEN Symmetry THEN NthHypEqTrans (-1) THEN Auto))
    )
   THEN (InstLemma `term-cases` [⌜opr⌝;⌜t⌝]⋅ THENA Auto)
   THEN D -1
   THEN ExRepD) }

1
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. v1 : varname()
7. ¬(v1 = nullvar() ∈ varname())
8. t = varterm(v1) ∈ term(opr)
⊢ t = varterm(v) ∈ term(opr)

2
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[v:\{v:varname()|  \mneg{}(v  =  nullvar())\}  ].  \mforall{}[t:term(opr)].
    t  =  varterm(v)  supposing  alpha-eq-terms(opr;varterm(v);t)


By

---

Latex:
((Auto
    THEN  (Assert  isvarterm(t)  =  tt  BY
                            ((FLemma  `isvarterm\_functionality`  [-1]  THENA  Auto)
                              THEN  Symmetry
                              THEN  NthHypEqTrans  (-1)
                              THEN  Auto))
    )
  THEN  (InstLemma  `term-cases`  [\mkleeneopen{}opr\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  ExRepD)

---

Home Index