A:Type, eq:EqDecider(A), P:(ATypeProp), f,g:x:A fp-> Type.
  ydom(f). w=f(y)   P(y,w)
  
  ydom(g). w=g(y)   P(y,w)  ydom(f  g). w=f  g(y)   P(y,w)

By:

UnivCD THEN Unfold `fpf-all` 0 THEN RWO Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A. Thm* x  dom(f  g)  x  dom(f)  x  dom(g) -1 THEN RWO Thm* eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A. Thm* f  g(x) ~ if x  dom(f) f(x) else g(x) fi 0 THEN SplitOnConclITE THEN All (Unfold `fpf-all`) THEN BackThruSomeHyp

1

1. A : Type 2. eq : EqDecider(A) 3. P : ATypeProp 4. f : x:A fp-> Type 5. g : x:A fp-> Type 6. y:A. y  dom(f)  P(y,f(y)) 7. y:A. y  dom(g)  P(y,g(y)) 8. y : A 9. y  dom(f)  y  dom(g) 10. y  dom(f)   y  dom(g)

1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html