---

Step * of Lemma fps-rng_wf

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng].  (fps-rng(r) ∈ CRng) supposing valueall-type(X)
BY
{ ((Auto THEN MemTypeCD) THEN Auto) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
⊢ fps-rng(r) ∈ Rng

2
.....set predicate..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
⊢ Comm(|fps-rng(r)|;*)

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].    (fps-rng(r)  \mmember{}  CRng)  supposing  valueall-type(X)


By

---

Latex:
((Auto  THEN  MemTypeCD)  THEN  Auto)

---

Home Index