---

Step * 1 1 of Lemma fpf-join-is-empty


1. A : Type
2. eq : EqDecider(A)
3. d1 : A List
⊢ (||filter(λa.tt;d1)|| =z 0) = (||d1|| =z 0)
BY
{ (RWO "filter_trivial" 0 THEN Auto) }

1
1. A : Type
2. eq : EqDecider(A)
3. d1 : A List
⊢ (∀x∈d1.↑λa.tt[x])

---

Latex:



1.  A  :  Type
2.  eq  :  EqDecider(A)
3.  d1  :  A  List
\mvdash{}  (||filter(\mlambda{}a.tt;d1)||  =\msubz{}  0)  =  (||d1||  =\msubz{}  0)


By

(RWO  "filter\_trivial"  0  THEN  Auto)

---

Home Index