---

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
{ (((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) }

---

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:
(((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)

---

Home Index