---

Step * 1 1 of Lemma fpf-compatible-singles


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])
9. x@0 : A@i
10. x = x@0 ∈ A@i
11. y = x@0 ∈ A@i
⊢ v = u ∈ B[x@0]
BY
{ (D (-4) THEN Auto)⋅ }

---

Latex:



1.  A  :  Type
2.  eq  :  EqDecider(A)
3.  B  :  A  {}\mrightarrow{}  Type
4.  x  :  A
5.  y  :  A
6.  v  :  B[x]
7.  u  :  B[y]
8.  (x  =  y)  {}\mRightarrow{}  (v  =  u)
9.  x@0  :  A@i
10.  x  =  x@0@i
11.  y  =  x@0@i
\mvdash{}  v  =  u


By

(D  (-4)  THEN  Auto)\mcdot{}

---

Home Index