---

Step * of Lemma min_l_tree_wf

∀[L,T:Type].  ∀t:l_tree(L;T). ∀f:T ⟶ ℤ.  (min_l_tree(t;f) ∈ T?)
BY
{ (ProveWfLemma THEN InstLemma `l_tree_covariant` [⌜L⌝;⌜Top⌝;⌜T⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L,T:Type].    \mforall{}t:l\_tree(L;T).  \mforall{}f:T  {}\mrightarrow{}  \mBbbZ{}.    (min\_l\_tree(t;f)  \mmember{}  T?)


By

---

Latex:
(ProveWfLemma  THEN  InstLemma  `l\_tree\_covariant`  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}Top\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index