---

Step * 1 of Lemma fpf-join-single-property


1. A : Type
2. B : A ─→ Type
3. f : a:A fp-> B[a]
4. a : A
5. v : B[a]
6. eq : EqDecider(A)
7. b : A
8. ¬(b = a ∈ A)
9. ↑b ∈ dom(f)
10. ↑b ∈ dom(f)
⊢ f ⊕ a : v(b) = f(b) ∈ B[b]
BY
{ ((RWO "fpf-join-ap-sq" 0 THEN Auto) THEN SplitOnConclITE THEN Auto) }

---

Latex:



1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  f  :  a:A  fp->  B[a]
4.  a  :  A
5.  v  :  B[a]
6.  eq  :  EqDecider(A)
7.  b  :  A
8.  \mneg{}(b  =  a)
9.  \muparrow{}b  \mmember{}  dom(f)
10.  \muparrow{}b  \mmember{}  dom(f)
\mvdash{}  f  \moplus{}  a  :  v(b)  =  f(b)


By

((RWO  "fpf-join-ap-sq"  0  THEN  Auto)  THEN  SplitOnConclITE  THEN  Auto)

---

Home Index