---

Step * of Lemma W_subtype

∀[A1,A2:Type]. ∀[B1:A1 ⟶ Type]. ∀[B2:A2 ⟶ Type].
  (W(A1;a.B1[a]) ⊆r W(A2;a.B2[a])) supposing ((∀a:A1. (B2[a] ⊆r B1[a])) and (A1 ⊆r A2))
BY
{ (Auto THEN D 0 THEN Auto THEN WElim (-1)) }

1
1. A1 : Type
2. A2 : Type
3. B1 : A1 ⟶ Type
4. B2 : A2 ⟶ Type
5. A1 ⊆r A2
6. ∀a:A1. (B2[a] ⊆r B1[a])
7. a : A1
8. f : B1[a] ⟶ W(A1;a.B1[a])
9. ∀b:B1[a]. (f b ∈ W(A2;a.B2[a]))
⊢ Wsup(a;f) ∈ W(A2;a.B2[a])

---

Latex:

---

Latex:
\mforall{}[A1,A2:Type].  \mforall{}[B1:A1  {}\mrightarrow{}  Type].  \mforall{}[B2:A2  {}\mrightarrow{}  Type].
    (W(A1;a.B1[a])  \msubseteq{}r  W(A2;a.B2[a]))  supposing  ((\mforall{}a:A1.  (B2[a]  \msubseteq{}r  B1[a]))  and  (A1  \msubseteq{}r  A2))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  WElim  (-1))

---

Home Index