---

Step * of Lemma l_disjoint-fpf-dom

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> Top]. ∀[L:A List].
  uiff(l_disjoint(A;fst(f);L);∀[a:A]. ¬(a ∈ L) supposing ↑a ∈ dom(f))
BY
{ (Unfolds ``fpf fpf-dom l_disjoint`` 0 THEN Auto) }

1
1. A : Type
2. eq : EqDecider(A)
3. f : d:A List × (a:{a:A| (a ∈ d)}  ─→ Top)
4. L : A List
5. ∀x:A. (¬((x ∈ fst(f)) ∧ (x ∈ L)))
6. a : A
7. ↑a ∈b fst(f))
⊢ ¬(a ∈ L)

2
1. A : Type
2. eq : EqDecider(A)
3. f : d:A List × (a:{a:A| (a ∈ d)}  ─→ Top)
4. L : A List
5. ∀[a:A]. ¬(a ∈ L) supposing ↑a ∈b fst(f))
6. x : A@i
⊢ ¬((x ∈ fst(f)) ∧ (x ∈ L))

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f:a:A  fp->  Top].  \mforall{}[L:A  List].
    uiff(l\_disjoint(A;fst(f);L);\mforall{}[a:A].  \mneg{}(a  \mmember{}  L)  supposing  \muparrow{}a  \mmember{}  dom(f))


By

(Unfolds  ``fpf  fpf-dom  l\_disjoint``  0  THEN  Auto)

---

Home Index