---

Step * of Lemma subtype_rel_list_set

∀[A,B:Type]. ∀[P:A ⟶ Type]. ∀[Q:B ⟶ Type].
  (({a:A| P[a]}  List) ⊆r ({b:B| Q[b]}  List)) supposing ((∀x:A. (P[x] ⇒ Q[x])) and ({a:A| P[a]}  ⊆r B))
BY
{ (Auto THEN Try ((SubsumeC ⌜{a:A| P[a]} ⌝⋅ THEN Complete (Auto))) THEN (BLemma `subtype_rel_list` THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[P:A  {}\mrightarrow{}  Type].  \mforall{}[Q:B  {}\mrightarrow{}  Type].
    ((\{a:A|  P[a]\}    List)  \msubseteq{}r  (\{b:B|  Q[b]\}    List))  supposing  ((\mforall{}x:A.  (P[x]  {}\mRightarrow{}  Q[x]))  and  (\{a:A|  P[a]\}    \msubseteq{}\000Cr  B))


By

---

Latex:
(Auto
  THEN  Try  ((SubsumeC  \mkleeneopen{}\{a:A|  P[a]\}  \mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
  THEN  (BLemma  `subtype\_rel\_list`  THEN  Auto)\mcdot{})

---

Home Index