---

Step * of Lemma strong-subtype-equal-lists

∀[A,B:Type].  ∀[L1:A List]. ∀[L2:B List].  L1 = L2 ∈ (A List) supposing L1 = L2 ∈ (B List) supposing strong-subtype(A;B)
BY
{ (BasicUniformUnivCD Auto
   THEN (FLemma `strong-subtype-implies` [3] THENA Auto)
   THEN BLemma `list_extensionality`
   THEN Auto
   THEN Try ((Symmetry THEN Complete (Auto))⋅)) }

1
.....wf..... 
1. A : Type
2. B : Type
3. strong-subtype(A;B)
4. L1 : A List
5. L2 : B List
6. L1 = L2 ∈ (B List)
7. ∀b:B. ∀a:A.  ((b = a ∈ B) ⇒ (b = a ∈ A))
⊢ L2 ∈ A List

---

Latex:

---

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


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  (FLemma  `strong-subtype-implies`  [3]  THENA  Auto)
  THEN  BLemma  `list\_extensionality`
  THEN  Auto
  THEN  Try  ((Symmetry  THEN  Complete  (Auto))\mcdot{}))

---

Home Index