---

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
{ xxx((UnivCD THENA Auto) THEN Unfold `fpf-all` 0 THEN Unfolds ``fpf-dom fpf-single fpf-ap`` 0 THEN Reduce 0)xxx }

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

---

Latex:

---

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

---

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

---

Home Index