---

Step * of Lemma fpf-cap_functionality

∀[A:Type]. ∀[d1,d2:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[x:A]. ∀[z:B[x]].  (f(x)?z = f(x)?z ∈ B[x])
BY
{ xxx(((Auto THEN Unfold `fpf-cap` 0 THEN SplitOnConclITE) THENA Auto)
      THEN SplitOnConclITE
      THEN Auto
      THEN D 5
      THEN (All (Unfold `fpf-dom`))
      THEN All Reduce
      THEN (All (RWO "assert-deq-member"))
      THEN Auto
      THEN Unfold `fpf-ap` 0
      THEN Reduce 0
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[d1,d2:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[x:A].  \mforall{}[z:B[x]].
    (f(x)?z  =  f(x)?z)


By

---

Latex:
xxx(((Auto  THEN  Unfold  `fpf-cap`  0  THEN  SplitOnConclITE)  THENA  Auto)
        THEN  SplitOnConclITE
        THEN  Auto
        THEN  D  5
        THEN  (All  (Unfold  `fpf-dom`))
        THEN  All  Reduce
        THEN  (All  (RWO  "assert-deq-member"))
        THEN  Auto
        THEN  Unfold  `fpf-ap`  0
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index