---

Step * 1 1 1 1 of Lemma fpf-join-sub2


1. A : Type
2. B : A ⟶ Type
3. eq : EqDecider(A)
4. f1 : a:A fp-> B[a]
5. g : a:A fp-> B[a]
6. f2 : a:A fp-> B[a]
7. ∀[g2:a:A fp-> B[a]]. (f1 ⊕ f2 ⊆ g ⊕ g2) supposing (f2 ⊆ g2 and f1 ⊆ g and f2 || g)
8. f1 ⊆ g
9. f2 ⊆ g
⊢ f2 || g
BY
{ xxx((All (Unfolds ``fpf-compatible fpf-sub``))
      THEN Auto
      THEN ∀h:hyp. ((InstHyp [⌜x⌝] h)⋅ THENA Complete (Auto)) 
      THEN ExRepD
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  eq  :  EqDecider(A)
4.  f1  :  a:A  fp->  B[a]
5.  g  :  a:A  fp->  B[a]
6.  f2  :  a:A  fp->  B[a]
7.  \mforall{}[g2:a:A  fp->  B[a]].  (f1  \moplus{}  f2  \msubseteq{}  g  \moplus{}  g2)  supposing  (f2  \msubseteq{}  g2  and  f1  \msubseteq{}  g  and  f2  ||  g)
8.  f1  \msubseteq{}  g
9.  f2  \msubseteq{}  g
\mvdash{}  f2  ||  g


By

---

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

---

Home Index