---

Step * 1 of Lemma fpf-cap-join-subtype


1. A : Type
2. eq : EqDecider(A)
3. f : a:A fp-> Type
4. g : a:A fp-> Type
5. a : A
⊢ f ⊕ g(a)?Top ⊆r f(a)?Top
BY
{ ((RWO "fpf-join-cap" 0 THENA Auto) THEN Unfold `fpf-cap` 0 THEN AutoSplit) }

---

Latex:



1.  A  :  Type
2.  eq  :  EqDecider(A)
3.  f  :  a:A  fp->  Type
4.  g  :  a:A  fp->  Type
5.  a  :  A
\mvdash{}  f  \moplus{}  g(a)?Top  \msubseteq{}r  f(a)?Top


By

((RWO  "fpf-join-cap"  0  THENA  Auto)  THEN  Unfold  `fpf-cap`  0  THEN  AutoSplit)

---

Home Index