---

Step * 1 of Lemma fpf-all-single-decl


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]
BY
{  Auto  }

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

---

Latex:



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


By

  Auto 

---

Home Index