---

Step * of Lemma fpf-all-single

∀[A:Type]
  ∀eq:EqDecider(A)
    ∀[B:A ─→ Type]. ∀[P:x:A ─→ B[x] ─→ ℙ].  ∀x:A. ∀v:B[x].  (∀y∈dom(x : v). w=x : v(y) ⇒  P[y;w] ⇐⇒ P[x;v])
BY
{ ((UnivCD THENA Auto) THEN Unfold `fpf-all` 0 THEN Unfolds ``fpf-dom fpf-single fpf-ap`` 0 THEN Reduce 0) }

1
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. [P] : x:A ─→ B[x] ─→ ℙ
5. x : A@i
6. v : B[x]@i
⊢ ∀y:A. ((↑((eq x y) ∨bff)) ⇒ P[y;v]) ⇐⇒ P[x;v]

---

Latex:


\mforall{}[A:Type]
    \mforall{}eq:EqDecider(A)
        \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[P:x:A  {}\mrightarrow{}  B[x]  {}\mrightarrow{}  \mBbbP{}].
            \mforall{}x:A.  \mforall{}v:B[x].    (\mforall{}y\mmember{}dom(x  :  v).  w=x  :  v(y)  {}\mRightarrow{}    P[y;w]  \mLeftarrow{}{}\mRightarrow{}  P[x;v])


By

((UnivCD  THENA  Auto)
  THEN  Unfold  `fpf-all`  0
  THEN  Unfolds  ``fpf-dom  fpf-single  fpf-ap``  0
  THEN  Reduce  0)

---

Home Index