---

Step * of Lemma free-1-iso_wf

∀[S:Type]. ∀[s:S]. ∀[K:CRng].  free-1-iso(s;K) ∈ free-vs(K;S) ≅ one-dim-vs(K) supposing ∀x,y:S.  (x = y ∈ S)
BY
{ (Auto THEN (Subst' free-1-iso(s;K) ~ TERMOF{free-vs-dim-1-ext:o, \\v:l, i:l} S s K 0 THENA Computation) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[s:S].  \mforall{}[K:CRng].
    free-1-iso(s;K)  \mmember{}  free-vs(K;S)  \mcong{}  one-dim-vs(K)  supposing  \mforall{}x,y:S.    (x  =  y)


By

---

Latex:
(Auto
  THEN  (Subst'  free-1-iso(s;K)  \msim{}  TERMOF\{free-vs-dim-1-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  S  s  K  0  THENA  Computation)
  THEN  Auto)

---

Home Index