---

Step * of Lemma subtype_rel_list-iff

∀[A,B:Type].  uiff((A List) ⊆r (B List);A ⊆r B)
BY
{ Auto }

1
1. A : Type
2. B : Type
3. (A List) ⊆r (B List)
⊢ A ⊆r B

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    uiff((A  List)  \msubseteq{}r  (B  List);A  \msubseteq{}r  B)


By

---

Latex:
Auto

---

Home Index