---

Step * 1 of Lemma strong-subtype_functionality


1. A1 : Type
2. B1 : Type
3. A2 : Type
4. B2 : Type
5. A1 ≡ A2@i
6. B1 ≡ B2@i
7. (A1 ⊆r B1) c∧ ({b:B1| ∃a:A1. (b = a ∈ B1)}  ⊆r A1)@i
8. A2 ⊆r B2
⊢ {b:B2| ∃a:A2. (b = a ∈ B2)}  ⊆r A2
BY
{ (D (-1) THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. A1 : Type
2. B1 : Type
3. A2 : Type
4. B2 : Type
5. A1 ≡ A2@i
6. B1 ≡ B2@i
7. (A1 ⊆r B1) c∧ ({b:B1| ∃a:A1. (b = a ∈ B1)}  ⊆r A1)@i
8. A2 ⊆r B2
9. x : {b:B2| ∃a:A2. (b = a ∈ B2)} @i
⊢ x ∈ A2

---

Latex:

---

Latex:

1.  A1  :  Type
2.  B1  :  Type
3.  A2  :  Type
4.  B2  :  Type
5.  A1  \mequiv{}  A2@i
6.  B1  \mequiv{}  B2@i
7.  (A1  \msubseteq{}r  B1)  c\mwedge{}  (\{b:B1|  \mexists{}a:A1.  (b  =  a)\}    \msubseteq{}r  A1)@i
8.  A2  \msubseteq{}r  B2
\mvdash{}  \{b:B2|  \mexists{}a:A2.  (b  =  a)\}    \msubseteq{}r  A2


By

---

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

---

Home Index