---

Step * of Lemma free-1-normal-form

∀[S:Type]
  ∀s:S. ∀x:Point(free-vs(ℤ-rng;S)).  ∃k:ℤ. (x = {<k, s>} ∈ Point(free-vs(ℤ-rng;S))) supposing ∀x,y:S.  (x = y ∈ S)
BY
{ (Auto THEN (InstLemma `free-iso-int_wf` [⌜S⌝;⌜s⌝]⋅ THENA Auto)) }

1
1. [S] : Type
2. ∀x,y:S.  (x = y ∈ S)
3. s : S
4. x : Point(free-vs(ℤ-rng;S))
5. free-iso-int(s) ∈ free-vs(ℤ-rng;S) ≅ ℤ
⊢ ∃k:ℤ. (x = {<k, s>} ∈ Point(free-vs(ℤ-rng;S)))

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}s:S.  \mforall{}x:Point(free-vs(\mBbbZ{}-rng;S)).    \mexists{}k:\mBbbZ{}.  (x  =  \{<k,  s>\})  supposing  \mforall{}x,y:S.    (x  =  y)


By

---

Latex:
(Auto  THEN  (InstLemma  `free-iso-int\_wf`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index