(4steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one one corr fams refl 1
1. A : Type
2. B : AType
  (x:A. B(x)) ~ (x:A. B(x))
By: Witness: Id | Id | u.Id | u.Id THEN Reduce 0

Generated subgoals:

1   InvFuns(A;A;Id;Id)
1 step
2 3. u : A
  InvFuns(B(u);B(u);Id;Id)
1 step

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

(4steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc