---

Step * of Lemma subtype-fpf-cap-void2

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. ∀[x:X]. ∀[z:g(x)?Void].  f(x)?Void ⊆r g(x)?Void supposing f || g
BY
{ ((Auto THEN (All (Unfolds ``fpf-compatible fpf-cap``)) THEN SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
1. X : Type
2. eq : EqDecider(X)
3. f : x:X fp-> Type
4. g : x:X fp-> Type
5. x : X
6. z : if x ∈ dom(g) then g(x) else Void fi 
7. ∀x:X. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ (f(x) = g(x) ∈ Type))
8. ↑x ∈ dom(f)
⊢ f(x) ⊆r if x ∈ dom(g) then g(x) else Void fi 

2
.....falsecase..... 
1. X : Type
2. eq : EqDecider(X)
3. f : x:X fp-> Type
4. g : x:X fp-> Type
5. x : X
6. z : if x ∈ dom(g) then g(x) else Void fi 
7. ∀x:X. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ (f(x) = g(x) ∈ Type))
8. ¬↑x ∈ dom(f)
⊢ Void ⊆r if x ∈ dom(g) then g(x) else Void fi 

---

Latex:


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


By

((Auto  THEN  (All  (Unfolds  ``fpf-compatible  fpf-cap``))  THEN  SplitOnConclITE)  THENA  Auto)

---

Home Index