---

Step * of Lemma fpf-single_wf2

∀[A,B:Type]. ∀[x:A]. ∀[v:B]. ∀[eqa:EqDecider(A)].  (x : v ∈ a:A fp-> x : B(a)?Top)
BY
{ Auto }

1
1. A : Type
2. B : Type
3. x : A
4. v : B
5. eqa : EqDecider(A)
6. a : A@i
⊢ x : B(a)?Top ∈ Type

---

Latex:


\mforall{}[A,B:Type].  \mforall{}[x:A].  \mforall{}[v:B].  \mforall{}[eqa:EqDecider(A)].    (x  :  v  \mmember{}  a:A  fp->  x  :  B(a)?Top)


By

Auto

---

Home Index