---

Step * of Lemma fpf-cap-subtype_functionality_wrt_sub2

∀[A1,A2,A3:Type]. ∀[d,d':EqDecider(A3)]. ∀[d2:EqDecider(A2)]. ∀[f:a:A1 fp-> Type]. ∀[g:a:A2 fp-> Type]. ∀[x:A3].
  ({g(x)?Top ⊆r f(x)?Top supposing f ⊆ g}) supposing (strong-subtype(A2;A3) and strong-subtype(A1;A2))
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN Try (FpfSubtype)
   THEN AssertBY strong-subtype(A1;A3)
      ((Using [`B',A2] (BLemma `strong-subtype_transitivity`))⋅ THEN Auto)⋅) }

1
1. A1 : Type
2. A2 : Type
3. A3 : Type
4. d : EqDecider(A3)
5. d' : EqDecider(A3)
6. d2 : EqDecider(A2)
7. f : a:A1 fp-> Type
8. g : a:A2 fp-> Type
9. x : A3
10. strong-subtype(A1;A2)
11. strong-subtype(A2;A3)
12. f ⊆ g
13. strong-subtype(A1;A3)
⊢ g(x)?Top ⊆r f(x)?Top

---

Latex:

---

Latex:
\mforall{}[A1,A2,A3:Type].  \mforall{}[d,d':EqDecider(A3)].  \mforall{}[d2:EqDecider(A2)].  \mforall{}[f:a:A1  fp->  Type].
\mforall{}[g:a:A2  fp->  Type].  \mforall{}[x:A3].
    (\{g(x)?Top  \msubseteq{}r  f(x)?Top  supposing  f  \msubseteq{}  g\})  supposing 
          (strong-subtype(A2;A3)  and 
          strong-subtype(A1;A2))


By

---

Latex:
(Unfold  `guard`  0
  THEN  Auto
  THEN  Try  (FpfSubtype)
  THEN  AssertBY  strong-subtype(A1;A3)
        ((Using  [`B',A2]  (BLemma  `strong-subtype\_transitivity`))\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index