---

Step * 1 of Lemma fpf-all-single


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]
BY
{ ( Auto  THEN (RW assert_pushdownC (-1)) THEN Auto THEN (D (-1)) THEN Auto) }

---

Latex:



1.  [A]  :  Type
2.  eq  :  EqDecider(A)@i
3.  [B]  :  A  {}\mrightarrow{}  Type
4.  [P]  :  x:A  {}\mrightarrow{}  B[x]  {}\mrightarrow{}  \mBbbP{}
5.  x  :  A@i
6.  v  :  B[x]@i
\mvdash{}  \mforall{}y:A.  ((\muparrow{}((eq  x  y)  \mvee{}\msubb{}ff))  {}\mRightarrow{}  P[y;v])  \mLeftarrow{}{}\mRightarrow{}  P[x;v]


By

(  Auto    THEN  (RW  assert\_pushdownC  (-1))  THEN  Auto  THEN  (D  (-1))  THEN  Auto)

---

Home Index