---

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
{ (Unfolds ``fpf-sub fpf-compatible`` 0
   THEN Auto
   THEN AllHyps h.(((InstHyp [⌈x⌉] h)⋅ THENM D -1) THENA Complete (Auto)) 
   THEN AllHyps h.((InstHyp [⌈x⌉] h)⋅ THEN Complete (Auto)) ) }

---

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

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

---

Home Index