Nuprl - Proof: fpf-all-single-decl

(13steps total) PrintForm Definitions Lemmas mb event system 4 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-all-single-decl

A:Type{i}, eq:EqDecider(A), P:(A

Type{i}

Prop{i}), x:A, v:Type{i}.

dom(x : v). w=x : v(y)

P(y,w)

P(x,v)

By:	Assert (A:Type{i'}, eq:EqDecider(A), B:(AType{i'}), P:(x:AB(x)Prop{i}), x:A, (v:B(x). ydom(x : v). w=x : v(y) P(y,w) P(x,v))

Generated subgoals:

1   A:Type{i'}, eq:EqDecider(A), B:(AType{i'}), P:(x:AB(x)Prop{i}), x:A,
  v:B(x). ydom(x : v). w=x : v(y)   P(y,w)  P(x,v)
11 steps

2 1. A:Type{i'}, eq:EqDecider(A), B:(AType{i'}), P:(x:AB(x)Prop{i}), x:A,
1. v:B(x). ydom(x : v). w=x : v(y)   P(y,w)  P(x,v)
  A:Type{i}, eq:EqDecider(A), P:(AType{i}Prop{i}), x:A, v:Type{i}.
  ydom(x : v). w=x : v(y)   P(y,w)  P(x,v)
1 step

About:

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

(13steps total) PrintForm Definitions Lemmas mb event system 4 Sections EventSystems Doc

1	A:Type{i'}, eq:EqDecider(A), B:(AType{i'}), P:(x:AB(x)Prop{i}), x:A, v:B(x). ydom(x : v). w=x : v(y) P(y,w) P(x,v)	11 steps
2	1. A:Type{i'}, eq:EqDecider(A), B:(AType{i'}), P:(x:AB(x)Prop{i}), x:A, 1. v:B(x). ydom(x : v). w=x : v(y) P(y,w) P(x,v) A:Type{i}, eq:EqDecider(A), P:(AType{i}Prop{i}), x:A, v:Type{i}. ydom(x : v). w=x : v(y) P(y,w) P(x,v)	1 step