---

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


1. [A] : Type
2. eq : EqDecider(A)
3. [P] : x:A ⟶ Type ⟶ ℙ
4. x : A
5. [v] : Type
6. P[x;v]
7. y : A
8. ↑((eq x y) ∨bff)
⊢ P[y;v]
BY
{ ((RW assert_pushdownC (-1)) THEN Auto THEN (D (-1)) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

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

---

Home Index