---

Step * of Lemma fpf-normalize_wf

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[g:x:A fp-> B[x]].  (fpf-normalize(eq;g) ∈ x:A fp-> B[x])
BY
{ xxx(Auto
      THEN (D (-1))
      THEN Unfold `fpf-normalize` 0
      THEN Reduce 0
      THEN (InstLemma `list-subtype` [⌜A⌝; ⌜d⌝])⋅
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[g:x:A  fp->  B[x]].
    (fpf-normalize(eq;g)  \mmember{}  x:A  fp->  B[x])


By

---

Latex:
xxx(Auto
        THEN  (D  (-1))
        THEN  Unfold  `fpf-normalize`  0
        THEN  Reduce  0
        THEN  (InstLemma  `list-subtype`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}d\mkleeneclose{}])\mcdot{}
        THEN  Auto)xxx

---

Home Index