---

Step * of Lemma fpf-cap-compatible

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. ∀[x:X].
  (f(x)?Void = g(x)?Void ∈ Type) supposing (g(x)?Void and f(x)?Void and f || g)
BY
{ (RepeatFor 6 ((D 0 THENA Auto)))⋅ }

1
1. X : Type
2. eq : EqDecider(X)
3. f : x:X fp-> Type
4. g : x:X fp-> Type
5. x : X
6. f || g
⊢ (f(x)?Void = g(x)?Void ∈ Type) supposing (g(x)?Void and f(x)?Void)

---

Latex:


\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].  \mforall{}[f,g:x:X  fp->  Type].  \mforall{}[x:X].
    (f(x)?Void  =  g(x)?Void)  supposing  (g(x)?Void  and  f(x)?Void  and  f  ||  g)


By

(RepeatFor  6  ((D  0  THENA  Auto)))\mcdot{}

---

Home Index