---

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@i
8. x1 : a:{a:A1| (a ∈ d)}  ─→ B1[a]@i
9. ∀b:A2. ∀a:A1.  ((b = a ∈ A2) ⇒ (b = a ∈ A1))
10. a : {a:A2| (a ∈ d)} 
⊢ x1 a ∈ B2[a]
BY
{ (((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) }

---

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@i
8.  x1  :  a:\{a:A1|  (a  \mmember{}  d)\}    {}\mrightarrow{}  B1[a]@i
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

(((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)

---

Home Index