---

Step * 1 of Lemma mkterm-one-one


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))}
BY
{ (RepUR ``coterm-fun mkterm`` -1
   THEN (FLemma `inr-one-one` [-1] THENA Auto)
   THEN (EqHD (-1) THENA Auto)
   THEN All Reduce
   THEN Unfold `guard` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  [Op]  :  Type
2.  term(Op)  \msubseteq{}r  coterm-fun(Op;term(Op))
3.  coterm-fun(Op;term(Op))  \msubseteq{}r  term(Op)
4.  [f]  :  Op
5.  [g]  :  Op
6.  [as]  :  (varname()  List  \mtimes{}  term(Op))  List
7.  [bs]  :  (varname()  List  \mtimes{}  term(Op))  List
8.  mkterm(f;as)  =  mkterm(g;bs)
9.  mkterm(f;as)  =  mkterm(g;bs)
\mvdash{}  \{(f  =  g)  \mwedge{}  (as  =  bs)\}


By

---

Latex:
(RepUR  ``coterm-fun  mkterm``  -1
  THEN  (FLemma  `inr-one-one`  [-1]  THENA  Auto)
  THEN  (EqHD  (-1)  THENA  Auto)
  THEN  All  Reduce
  THEN  Unfold  `guard`  0
  THEN  Auto)

---

Home Index