---

Step * 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])
⊢ x : v || y : u
BY
{ (Repeat ((Unfolds ``fpf-ap fpf-compatible fpf-dom fpf-single eqof`` 0 THEN Reduce 0))
   THEN Intros
   THEN D -1
   THEN (RW assert_pushdownC 10 THENA Auto)
   THEN (RW assert_pushdownC 11 THENA Auto)
   THEN Auto) }

---

Latex:

---

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)
\mvdash{}  x  :  v  ||  y  :  u


By

---

Latex:
(Repeat  ((Unfolds  ``fpf-ap  fpf-compatible  fpf-dom  fpf-single  eqof``  0  THEN  Reduce  0))
  THEN  Intros
  THEN  D  -1
  THEN  (RW  assert\_pushdownC  10  THENA  Auto)
  THEN  (RW  assert\_pushdownC  11  THENA  Auto)
  THEN  Auto)

---

Home Index