---

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 Auto
   THEN AllHyps h.(((RW assert_pushdownC h THENA Auto) THEN ElimOrFalse h) 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])
9. x@0 : A@i
10. x = x@0 ∈ A@i
11. y = x@0 ∈ A@i
⊢ v = u ∈ B[x@0]

---

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

(Repeat  ((Unfolds  ``fpf-ap  fpf-compatible  fpf-dom  fpf-single  eqof``  0  THEN  Reduce  0))
  THEN  Auto
  THEN  AllHyps  h.(((RW  assert\_pushdownC  h  THENA  Auto)  THEN  ElimOrFalse  h)  THENA  Auto)  )

---

Home Index