Nuprl - Proof: fpf-join-ap

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-join-ap

A:Type, B:(A

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

dom(f

g(x) = if x

dom(f)

f(x) else g(x) fi

B(x)

By:	Auto THEN Unfolds [`fpf-join`;`fpf-ap`] 0 THEN Reduce 0 THEN Subst ((2of(f)(x)) ~ f(x)) 0 THEN Try (Unfold `fpf-ap` 0 THEN Trivial) THEN Subst ((2of(g)(x)) ~ g(x)) 0 THEN Try (Unfold `fpf-ap` 0 THEN Trivial) THEN Unfold `fpf-cap` 0 THEN Fold `member` 0 THEN SplitOnConclITE

Generated subgoal:

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

About:

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