---

Step * of Lemma l_tree_covariant

∀[A,B,T:Type].  l_tree(A;T) ⊆r l_tree(B;T) supposing A ⊆r B
BY
{ Auto }

1
1. A : Type
2. B : Type
3. T : Type
4. A ⊆r B
⊢ l_tree(A;T) ⊆r l_tree(B;T)

---

Latex:


\mforall{}[A,B,T:Type].    l\_tree(A;T)  \msubseteq{}r  l\_tree(B;T)  supposing  A  \msubseteq{}r  B


By

Auto

---

Home Index