---

Step * of Lemma fpf-all-empty

∀[A:Type]. ∀eq,P:Top.  (∀y∈dom(⊗). w=⊗(y) ⇒  P[y;w] ⇐⇒ True)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``fpf-all fpf-empty fpf-dom`` 0) }

1
1. [A] : Type
2. eq : Top@i
3. P : Top@i
⊢ ∀y:A. (False ⇒ P[y;⋅]) ⇐⇒ True

---

Latex:


\mforall{}[A:Type].  \mforall{}eq,P:Top.    (\mforall{}y\mmember{}dom(\motimes{}).  w=\motimes{}(y)  {}\mRightarrow{}    P[y;w]  \mLeftarrow{}{}\mRightarrow{}  True)


By

((UnivCD  THENA  Auto)  THEN  RepUR  ``fpf-all  fpf-empty  fpf-dom``  0)

---

Home Index