---

Step * 1 of Lemma before_wf


1. a : DSet
2. ps : |a| List
3. u : |a|
⊢ null(ps) ∨b(hd(ps) <b u) ∈ 𝔹
BY
{ ((D 2 THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  DSet
2.  ps  :  |a|  List
3.  u  :  |a|
\mvdash{}  null(ps)  \mvee{}\msubb{}(hd(ps)  <\msubb{}  u)  \mmember{}  \mBbbB{}


By

---

Latex:
((D  2  THEN  Reduce  0)  THEN  Auto)

---

Home Index