---

Step * 1 of Lemma subtype-fpf3


1. A1 : Type
2. A2 : Type
3. B1 : A1 ⟶ Type
4. B2 : A2 ⟶ Type
5. strong-subtype(A1;A2)
6. ∀a:A1. (B1[a] ⊆r B2[a])
7. d : A1 List
8. x1 : a:{a:A1| (a ∈ d)}  ⟶ B1[a]
9. ∀b:A2. ∀a:A1.  ((b = a ∈ A2) ⇒ (b = a ∈ A1))
10. a : {a:A2| (a ∈ d)} 
⊢ x1 a ∈ B2[a]
BY
{ xxx(((D -1 THEN FLemma `strong-subtype-l_member-type` [5;-1]) THENA Auto)
      THEN SubsumeC ⌜B1[a]⌝⋅
      THEN Auto
      THEN FLemma `strong-subtype-l_member` [5;-2]
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  A1  :  Type
2.  A2  :  Type
3.  B1  :  A1  {}\mrightarrow{}  Type
4.  B2  :  A2  {}\mrightarrow{}  Type
5.  strong-subtype(A1;A2)
6.  \mforall{}a:A1.  (B1[a]  \msubseteq{}r  B2[a])
7.  d  :  A1  List
8.  x1  :  a:\{a:A1|  (a  \mmember{}  d)\}    {}\mrightarrow{}  B1[a]
9.  \mforall{}b:A2.  \mforall{}a:A1.    ((b  =  a)  {}\mRightarrow{}  (b  =  a))
10.  a  :  \{a:A2|  (a  \mmember{}  d)\} 
\mvdash{}  x1  a  \mmember{}  B2[a]


By

---

Latex:
xxx(((D  -1  THEN  FLemma  `strong-subtype-l\_member-type`  [5;-1])  THENA  Auto)
        THEN  SubsumeC  \mkleeneopen{}B1[a]\mkleeneclose{}\mcdot{}
        THEN  Auto
        THEN  FLemma  `strong-subtype-l\_member`  [5;-2]
        THEN  Auto)xxx

---

Home Index