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

By:	Unfolds [`fpf`;`fpf-join`] 0 THEN Try (Unfold `fpf-dom` 0) THEN All (i.Fold `fpf` i THEN Complete Auto) THEN AssertBY (f  a:A fp-> B(a)) (All (i.Fold `fpf` i THEN Complete Auto)) THEN AssertBY (g  a:A fp-> B(a)) (All (i.Fold `fpf` i THEN Complete Auto))

1

1. A : Type 2. B : AType 3. f : d:A Lista:{a:A| (a  d) }B(a) 4. g : d:A Lista:{a:A| (a  d) }B(a) 5. eq : EqDecider(A) 6. a : {a:A| (a  1of(f) @ filter(a.a  dom(f);1of(g))) } 7. f  a:A fp-> B(a) 8. g  a:A fp-> B(a)   f(a)?g(a)  B(a)

10 steps

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