Nuprl - Proof: ext axiom

(4steps total) PrintForm Definitions hol Sections HOLlib Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ext axiom

A,B:Type. A = B

B & B

By:	StrongAuto

Generated subgoals:

1 1. A : Type
2. B : Type
3. A = B
  A  B
1 step

2 1. A : Type
2. B : Type
3. A = B
  B  A
1 step

3 1. A : Type
2. B : Type
3. A  B
4. B  A
  A = B
Fiat

About:

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

(4steps total) PrintForm Definitions hol Sections HOLlib Doc

1	1. A : Type 2. B : Type 3. A = B A B	1 step
2	1. A : Type 2. B : Type 3. A = B B A	1 step
3	1. A : Type 2. B : Type 3. A B 4. B A A = B	Fiat