---

Step * 1 1 of Lemma fps-rng_wf


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
⊢ fps-rng(r) ∈ RngSig
BY
{ (Unfold `rng_sig` 0 THEN ProveWfLemma THEN (D 1 THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
\mvdash{}  fps-rng(r)  \mmember{}  RngSig


By

---

Latex:
(Unfold  `rng\_sig`  0  THEN  ProveWfLemma  THEN  (D  1  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index