---

Step * of Lemma bs_l_tree_member_wf

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

---

Latex:


\mforall{}[L,T:Type].  \mforall{}[t:l\_tree(L;T)].  \mforall{}[x:T].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].    (bs\_l\_tree\_member(x;t;f)  \mmember{}  \mBbbB{})


By

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

---

Home Index