---

Step * of Lemma max_l_tree_wf

∀[L,T:Type].  ∀t:l_tree(L;T). ∀f:T ─→ ℤ.  (max_l_tree(t;f) ∈ T?)
BY
{ (ProveWfLemma THEN InstLemma `l_tree_covariant` [⌈L⌉;⌈Top⌉;⌈T⌉]⋅ THEN Auto) }

---

Latex:


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


By

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

---

Home Index