(22steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-sub-functionality 1 2 2 2

1. A : Type
2. A' : Type
3. strong-subtype(A;A')
4. B : AType
5. C : A'Type
6. eq : EqDecider(A)
7. eq' : EqDecider(A')
8. f : a:A fp-> B(a)
9. g : a:A fp-> B(a)
10. A A'
11. eq'  EqDecider(A)
12. a:AB(aC(a)
13. x:Ax  dom(f x  dom(g) & f(x) = g(x)
14. x : A
15. x  dom(f)
16. x  A
17. x  dom(g)
18. f(x) = g(x)
19. x  dom(g)
  f(x) = g(x C(x)


By: All (Unfold `fpf-ap`) THEN HypSubst -2 0


Generated subgoals:

1 13. x:Ax  dom(f x  dom(g) & 2of(f)(x) = 2of(g)(x B(x)
14. x : A
15. x  dom(f)
16. x  A
17. x  dom(g)
18. 2of(f)(x) = 2of(g)(x B(x)
19. x  dom(g)
  2of(g)(x) = 2of(g)(x C(x)

5 steps
2 13. x:Ax  dom(f x  dom(g) & 2of(f)(x) = 2of(g)(x B(x)
14. x : A
15. x  dom(f)
16. x  A
17. x  dom(g)
18. 2of(f)(x) = 2of(g)(x B(x)
19. x  dom(g)
20. z : B(x)
  (z = 2of(g)(x C(x))  Prop

8 steps

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

(22steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc