---

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


1. A : Type
2. eq : EqDecider(A)
3. d1 : A List
⊢ (∀x∈d1.↑λa.tt[x])
BY
{ (Unfold `l_all` 0 THEN ReduceSOAps 0 THEN Reduce 0 THEN Auto) }

---

Latex:



1.  A  :  Type
2.  eq  :  EqDecider(A)
3.  d1  :  A  List
\mvdash{}  (\mforall{}x\mmember{}d1.\muparrow{}\mlambda{}a.tt[x])


By

(Unfold  `l\_all`  0  THEN  ReduceSOAps  0  THEN  Reduce  0  THEN  Auto)

---

Home Index