---

Step * of Lemma fpf-single_wf

∀[A:𝕌{j}]. ∀[B:A ─→ Type]. ∀[x:A]. ∀[v:B[x]].  (x : v ∈ x:A fp-> B[x])
BY
{ (Unfolds ``fpf fpf-single`` 0
   THEN Auto
   THEN (RWO "member_singleton" (-1))
   THEN Auto
   THEN Assert ⌈(B x1) = (B x) ∈ Type⌉⋅
   THEN Auto
   THEN EqCD
   THEN Auto) }

---

Latex:


\mforall{}[A:\mBbbU{}\{j\}].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[x:A].  \mforall{}[v:B[x]].    (x  :  v  \mmember{}  x:A  fp->  B[x])


By

(Unfolds  ``fpf  fpf-single``  0
  THEN  Auto
  THEN  (RWO  "member\_singleton"  (-1))
  THEN  Auto
  THEN  Assert  \mkleeneopen{}(B  x1)  =  (B  x)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index