---

Step * of Lemma fpf-compatible-singles

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ─→ Type]. ∀[x,y:A]. ∀[v:B[x]]. ∀[u:B[y]].
  x : v || y : u supposing (x = y ∈ A) ⇒ (v = u ∈ B[x])
BY
{ (UnivCD THENA Auto) }

1
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. x : A
5. y : A
6. v : B[x]
7. u : B[y]
8. (x = y ∈ A) ⇒ (v = u ∈ B[x])
⊢ x : v || y : u

---

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]].
    x  :  v  ||  y  :  u  supposing  (x  =  y)  {}\mRightarrow{}  (v  =  u)


By

(UnivCD  THENA  Auto)

---

Home Index