---

Step * 1 of Lemma fpf-cap-compatible


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)
BY
{ (((Unfold `fpf-cap` 0 THEN SplitOnConclITE) THENM SplitOnConclITE) THEN Auto) }

---

Latex:



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
\mvdash{}  (f(x)?Void  =  g(x)?Void)  supposing  (g(x)?Void  and  f(x)?Void)


By

(((Unfold  `fpf-cap`  0  THEN  SplitOnConclITE)  THENM  SplitOnConclITE)  THEN  Auto)

---

Home Index