A:Type, eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a).
  h || f  h || g  h || f  g

1

1. A : Type 2. eq : EqDecider(A) 3. B : AType 4. f : a:A fp-> B(a) 5. g : a:A fp-> B(a) 6. h : a:A fp-> B(a) 7. x:A. x  dom(h) & x  dom(f)  h(x) = f(x)  B(x) 8. x:A. x  dom(h) & x  dom(g)  h(x) = g(x)  B(x) 9. x : A   x  dom(h) & x  dom(f  g)  h(x) = f  g(x)  B(x)

2 steps

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