---

Step * of Lemma fpf-empty-join

∀[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) }

1
1. A : Type
2. B : A ─→ Type
3. d : A List
4. f1 : a:{a:A| (a ∈ d)}  ─→ B[a]
5. eq : EqDecider(A)
⊢ (λa.if a ∈b d) then f1 a else ⋅ fi ) = f1 ∈ (a:{a:A| (a ∈ d)}  ─→ B[a])

---

Latex:


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


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)

---

Home Index