---

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:

---

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

---

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

---

Home Index