IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-sub-join-right1 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. f || g 7. x : A 8. x dom(g)
9. x dom(f)
g(x) = f(x) B(x)
By:
Unfold `fpf-compatible` -4 THEN InstHyp [x] -4
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
dom(g)
g(x) = f(x) 
