---

Step * of Lemma fpf-compatible_monotonic

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f1,g1,f2,g2:a:A fp-> B[a]].
  (f1 || g1) supposing (f2 || g2 and g1 ⊆ g2 and f1 ⊆ f2)
BY
{ xxx(Unfolds ``fpf-sub fpf-compatible`` 0
      THEN Auto
      THEN ∀h:hyp. xxx(((InstHyp [⌜x⌝] h)⋅ THENM D -1) THENA Complete (Auto))xxx 
      THEN ∀h:hyp. xxx((InstHyp [⌜x⌝] h)⋅ THEN Complete (Auto))xxx )xxx }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f1,g1,f2,g2:a:A  fp->  B[a]].
    (f1  ||  g1)  supposing  (f2  ||  g2  and  g1  \msubseteq{}  g2  and  f1  \msubseteq{}  f2)


By

---

Latex:
xxx(Unfolds  ``fpf-sub  fpf-compatible``  0
        THEN  Auto
        THEN  \mforall{}h:hyp.  xxx(((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h)\mcdot{}  THENM  D  -1)  THENA  Complete  (Auto))xxx 
        THEN  \mforall{}h:hyp.  xxx((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h)\mcdot{}  THEN  Complete  (Auto))xxx  )xxx

---

Home Index