---

Step * of Lemma strong-subtype-list

∀[A,B:Type].  strong-subtype(A List;B List) supposing strong-subtype(A;B)
BY
{ ((UnivCD THENA Auto)
   THEN ∀h:hyp. ((FLemma `strong-subtype-implies` [h] THENA Auto) THEN D h) 
   THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. A ⊆r B
4. {b:B| ∃a:A. (b = a ∈ B)}  ⊆r A
5. ∀b:B. ∀a:A.  ((b = a ∈ B) ⇒ (b = a ∈ A))
6. (A List) ⊆r (B List)
7. x : {b:B List| ∃a:A List. (b = a ∈ (B List))} 
⊢ x ∈ A List

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    strong-subtype(A  List;B  List)  supposing  strong-subtype(A;B)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  \mforall{}h:hyp.  ((FLemma  `strong-subtype-implies`  [h]  THENA  Auto)  THEN  D  h) 
  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index