---

Step * of Lemma fpf-sub-join-left2

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,h,g:a:A fp-> B[a]].  h ⊆ f ⊕ g supposing h ⊆ f
BY
{ (Auto
   THEN (InstLemma `fpf-sub_transitivity` [⌜A⌝; ⌜B⌝; ⌜eq⌝; ⌜h⌝; ⌜f⌝; ⌜f ⊕ g⌝])⋅
   THEN Auto
   THEN (Using [`B2',⌜B⌝] (BLemma `fpf-sub-join-left`)⋅ THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f,h,g:a:A  fp->  B[a]].    h  \msubseteq{}  f  \moplus{}  g  supposing  h  \msubseteq{}  f


By

---

Latex:
(Auto
  THEN  (InstLemma  `fpf-sub\_transitivity`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}h\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}f  \moplus{}  g\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  (Using  [`B2',\mkleeneopen{}B\mkleeneclose{}]  (BLemma  `fpf-sub-join-left`)\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index