---

Step * of Lemma fpf-compatible-join

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ─→ Type]. ∀[f,g,h:a:A fp-> B[a]].  (h || f ⊕ g) supposing (h || g and h || f)
BY
{ ((Auto THEN (All (Unfold `fpf-compatible`)) THEN D 0) THENA Auto) }

1
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. f : a:A fp-> B[a]
5. g : a:A fp-> B[a]
6. h : a:A fp-> B[a]
7. ∀x:A. (((↑x ∈ dom(h)) ∧ (↑x ∈ dom(f))) ⇒ (h(x) = f(x) ∈ B[x]))
8. ∀x:A. (((↑x ∈ dom(h)) ∧ (↑x ∈ dom(g))) ⇒ (h(x) = g(x) ∈ B[x]))
9. x : A@i
⊢ ((↑x ∈ dom(h)) ∧ (↑x ∈ dom(f ⊕ g))) ⇒ (h(x) = f ⊕ g(x) ∈ B[x])

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f,g,h:a:A  fp->  B[a]].
    (h  ||  f  \moplus{}  g)  supposing  (h  ||  g  and  h  ||  f)


By

((Auto  THEN  (All  (Unfold  `fpf-compatible`))  THEN  D  0)  THENA  Auto)

---

Home Index