Nuprl - Proof: simple card cross assoc 1 1

(11steps total) Remark PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: simple card cross assoc 1 1

1. A : Type
2. B : Type
3. C : Type

InvFuns(A

C;(A

InvFuns;

abc.abc/a,bc. bc/b,c. <<a,b>,c>;

xyz.xyz/xy,z. xy/x,y. <x,y,z>)

By:	Analyze THENL [New:abc Analyze;New:xyz Analyze]

Generated subgoals:

1 4. abc : ABC
  (xyz.xyz/xy,z. xy/x,y. <x,y,z>)((abc.abc/a,bc. bc/b,c. <<a,b>,c>)(abc))
  =
  abc
4 steps

2 4. xyz : (AB)C
  (abc.abc/a,bc. bc/b,c. <<a,b>,c>)((xyz.xyz/xy,z. xy/x,y. <x,y,z>)(xyz))
  =
  xyz
4 steps

About:

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

(11steps total) Remark PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

1	4. abc : ABC (xyz.xyz/xy,z. xy/x,y. <x,y,z>)((abc.abc/a,bc. bc/b,c. <<a,b>,c>)(abc)) = abc	4 steps
2	4. xyz : (AB)C (abc.abc/a,bc. bc/b,c. <<a,b>,c>)((xyz.xyz/xy,z. xy/x,y. <x,y,z>)(xyz)) = xyz	4 steps