---

Step * of Lemma fpf-empty-join

No Annotations
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[eq:EqDecider(A)].  (f ⊕ ⊗ = f ∈ a:A fp-> B[a])
BY
{ (Auto
   THEN DVar `f'
   THEN RepUR ``fpf-join fpf-empty fpf-cap fpf-dom fpf-ap fpf`` 0
   THEN EqCD
   THEN Auto
   THEN RWO "append-nil" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[eq:EqDecider(A)].    (f  \moplus{}  \motimes{}  =  f)


By

---

Latex:
(Auto
  THEN  DVar  `f'
  THEN  RepUR  ``fpf-join  fpf-empty  fpf-cap  fpf-dom  fpf-ap  fpf``  0
  THEN  EqCD
  THEN  Auto
  THEN  RWO  "append-nil"  0
  THEN  Auto)

---

Home Index