---

Step * of Lemma subtype-fpf3

∀[A1,A2:Type]. ∀[B1:A1 ─→ Type]. ∀[B2:A2 ─→ Type].
  (a:A1 fp-> B1[a] ⊆r a:A2 fp-> B2[a]) supposing ((∀a:A1. (B1[a] ⊆r B2[a])) and strong-subtype(A1;A2))
BY
{ (Intros
   THEN (D 0 THENA Auto)
   THEN (FLemma `strong-subtype-implies` [-3] THENA Auto)
   THEN ParallelOp -2
   THEN D -2
   THEN MemCD
   THEN Try (QuickAuto)
   THEN (ExtWith [`a'] [a:{a:A1| (a ∈ d)}  ─→ B1[a]])⋅
   THEN Try (QuickAuto)) }

1
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]

---

Latex:


\mforall{}[A1,A2:Type].  \mforall{}[B1:A1  {}\mrightarrow{}  Type].  \mforall{}[B2:A2  {}\mrightarrow{}  Type].
    (a:A1  fp->  B1[a]  \msubseteq{}r  a:A2  fp->  B2[a])  supposing 
          ((\mforall{}a:A1.  (B1[a]  \msubseteq{}r  B2[a]))  and 
          strong-subtype(A1;A2))


By

(Intros
  THEN  (D  0  THENA  Auto)
  THEN  (FLemma  `strong-subtype-implies`  [-3]  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  D  -2
  THEN  MemCD
  THEN  Try  (QuickAuto)
  THEN  (ExtWith  [`a']  [a:\{a:A1|  (a  \mmember{}  d)\}    {}\mrightarrow{}  B1[a]])\mcdot{}
  THEN  Try  (QuickAuto))

---

Home Index