Nuprl - Proof: inv pair inv 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inv pair inv 1

1. A : Type
2. B : Type

B) ~ (A ~ B)

By:	(fg.fg/f,g. <f,g,(x.``),(y.``)>) (AB)(A ~ B) \| (fga.fga/f,#. #/g,a. <f,g>) (A ~ B)AB Asserted

Generated subgoals:

1   (fg.fg/f,g. <f,g,(x.*),(y.*)>)  (AB)(A ~ B)
3 steps

2 3. (fg.fg/f,g. <f,g,(x.*),(y.*)>)  (AB)(A ~ B)
  (fga.fga/f,#. #/g,a. <f,g>)  (A ~ B)AB
3 steps

3 3. (fg.fg/f,g. <f,g,(x.*),(y.*)>)  (AB)(A ~ B)
4. (fga.fga/f,#. #/g,a. <f,g>)  (A ~ B)AB
  (AB) ~ (A ~ B)
19 steps

About:

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

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

1	(fg.fg/f,g. <f,g,(x.``),(y.``)>) (AB)(A ~ B)	3 steps
2	3. (fg.fg/f,g. <f,g,(x.``),(y.``)>) (AB)(A ~ B) (fga.fga/f,#. #/g,a. <f,g>) (A ~ B)AB	3 steps
3	3. (fg.fg/f,g. <f,g,(x.``),(y.``)>) (AB)(A ~ B) 4. (fga.fga/f,#. #/g,a. <f,g>) (A ~ B)AB (AB) ~ (A ~ B)	19 steps