---

Step * of Lemma compare-fun_wf

∀[A,B:Type]. ∀[cmp:comparison(B)]. ∀[f:A ⟶ B].  (compare-fun(cmp;f) ∈ comparison(A))
BY
{ (ProveWfLemma THEN D -2 THEN MemTypeCD THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[cmp:comparison(B)].  \mforall{}[f:A  {}\mrightarrow{}  B].    (compare-fun(cmp;f)  \mmember{}  comparison(A))


By

---

Latex:
(ProveWfLemma  THEN  D  -2  THEN  MemTypeCD  THEN  All  Reduce  THEN  Auto)

---

Home Index