---

Step * of Lemma mkterm-one-one

No Annotations
∀[Op:Type]. ∀[f,g:Op]. ∀[as,bs:(varname() List × term(Op)) List].
  ((mkterm(f;as) = mkterm(g;bs) ∈ term(Op)) ⇒ {(f = g ∈ Op) ∧ (as = bs ∈ ((varname() List × term(Op)) List))})
BY
{ (InstLemma `term-ext` []
   THEN ParallelLast'
   THEN D -1
   THEN Intros
   THEN (Assert mkterm(f;as) = mkterm(g;bs) ∈ coterm-fun(Op;term(Op)) BY
               Auto)) }

1
1. [Op] : Type
2. term(Op) ⊆r coterm-fun(Op;term(Op))
3. coterm-fun(Op;term(Op)) ⊆r term(Op)
4. [f] : Op
5. [g] : Op
6. [as] : (varname() List × term(Op)) List
7. [bs] : (varname() List × term(Op)) List
8. mkterm(f;as) = mkterm(g;bs) ∈ term(Op)
9. mkterm(f;as) = mkterm(g;bs) ∈ coterm-fun(Op;term(Op))
⊢ {(f = g ∈ Op) ∧ (as = bs ∈ ((varname() List × term(Op)) List))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Op:Type].  \mforall{}[f,g:Op].  \mforall{}[as,bs:(varname()  List  \mtimes{}  term(Op))  List].
    ((mkterm(f;as)  =  mkterm(g;bs))  {}\mRightarrow{}  \{(f  =  g)  \mwedge{}  (as  =  bs)\})


By

---

Latex:
(InstLemma  `term-ext`  []
  THEN  ParallelLast'
  THEN  D  -1
  THEN  Intros
  THEN  (Assert  mkterm(f;as)  =  mkterm(g;bs)  BY
                          Auto))

---

Home Index