---

Step * of Lemma fpf-contains-union-join-left2

∀[A:Type]. ∀[B:A ─→ Type].
  ∀eq:EqDecider(A). ∀f,h,g:a:A fp-> B[a] List. ∀R:∩a:A. ((B[a] List) ─→ B[a] ─→ 𝔹).
    (h ⊆⊆ f ⇒ h ⊆⊆ fpf-union-join(eq;R;f;g))
BY
{ (Auto THEN RepeatFor 3 (ParallelLast) THEN Auto) }

1
1. [A] : Type
2. [B] : A ─→ Type
3. eq : EqDecider(A)@i
4. f : a:A fp-> B[a] List@i
5. h : a:A fp-> B[a] List@i
6. g : a:A fp-> B[a] List@i
7. R : ∩a:A. ((B[a] List) ─→ B[a] ─→ 𝔹)@i
8. ∀x:A. ((↑x ∈ dom(h)) ⇒ ((↑x ∈ dom(f)) c∧ h(x) ⊆ f(x)))@i
9. x : A@i
10. ↑x ∈ dom(h)@i
11. (↑x ∈ dom(f)) c∧ h(x) ⊆ f(x)
⊢ ↑x ∈ dom(fpf-union-join(eq;R;f;g))

2
1. [A] : Type
2. [B] : A ─→ Type
3. eq : EqDecider(A)@i
4. f : a:A fp-> B[a] List@i
5. h : a:A fp-> B[a] List@i
6. g : a:A fp-> B[a] List@i
7. R : ∩a:A. ((B[a] List) ─→ B[a] ─→ 𝔹)@i
8. ∀x:A. ((↑x ∈ dom(h)) ⇒ ((↑x ∈ dom(f)) c∧ h(x) ⊆ f(x)))@i
9. x : A@i
10. ↑x ∈ dom(h)@i
11. (↑x ∈ dom(f)) c∧ h(x) ⊆ f(x)
12. ↑x ∈ dom(fpf-union-join(eq;R;f;g))
⊢ h(x) ⊆ fpf-union-join(eq;R;f;g)(x)

---

Latex:


\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}eq:EqDecider(A).  \mforall{}f,h,g:a:A  fp->  B[a]  List.  \mforall{}R:\mcap{}a:A.  ((B[a]  List)  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbB{}).
        (h  \msubseteq{}\msubseteq{}  f  {}\mRightarrow{}  h  \msubseteq{}\msubseteq{}  fpf-union-join(eq;R;f;g))


By

(Auto  THEN  RepeatFor  3  (ParallelLast)  THEN  Auto)

---

Home Index