---

Step * of Lemma term-ext

No Annotations
∀[opr:Type]. term(opr) ≡ coterm-fun(opr;term(opr))
BY
{ (Auto THEN (InstLemma `coterm-ext` [⌜opr⌝]⋅ THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
.....subterm..... T:t
1:n
1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. x : term(opr)
⊢ x ∈ coterm-fun(opr;term(opr))

2
.....subterm..... T:t
1:n
1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. x : coterm-fun(opr;term(opr))
⊢ x ∈ term(opr)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  term(opr)  \mequiv{}  coterm-fun(opr;term(opr))


By

---

Latex:
(Auto  THEN  (InstLemma  `coterm-ext`  [\mkleeneopen{}opr\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index