---

Step * of Lemma fpf-all-single-decl

∀[A:Type]. ∀eq:EqDecider(A). ∀[P:x:A ─→ Type ─→ ℙ]. ∀x:A. ∀[v:Type]. (∀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. [P] : x:A ─→ Type ─→ ℙ
4. x : A@i
5. [v] : Type
⊢ ∀y:A. ((↑((eq x y) ∨bff)) ⇒ P[y;v]) ⇐⇒ P[x;v]

---

Latex:


\mforall{}[A:Type]
    \mforall{}eq:EqDecider(A)
        \mforall{}[P:x:A  {}\mrightarrow{}  Type  {}\mrightarrow{}  \mBbbP{}].  \mforall{}x:A.  \mforall{}[v:Type].  (\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