---

Step * 1 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
6. P[x;v]@i
7. y : A@i
8. ↑((eq x y) ∨bff)@i
⊢ P[y;v]
BY
{ ((RW assert_pushdownC (-1)) THEN Auto THEN (D (-1)) THEN Auto) }

---

Latex:



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


By

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

---

Home Index