---

Step * of Lemma fpf-compatible-singles-iff

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[x,y:A]. ∀[v:B[x]]. ∀[u:B[y]].
  uiff(x : v || y : u;v = u ∈ B[x] supposing x = y ∈ A)
BY
{ Auto⋅ }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[x,y:A].  \mforall{}[v:B[x]].  \mforall{}[u:B[y]].
    uiff(x  :  v  ||  y  :  u;v  =  u  supposing  x  =  y)


By

---

Latex:
Auto\mcdot{}

---

Home Index