(8steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: rel-graph functionality 2
1. T: Type
2. R1: TTProp
3. R2: TTProp
4. x,y:T. R1(x,y) R2(x,y)
Bij({p:(TT)| R1(1of(p),2of(p)) }; {p:(TT)| R2(1of(p),2of(p)) }; Id)
By:
Unfold `biject` 0
THEN
Unfolds [`inject`;`surject`] 0
THEN
Reduce 0
Generated subgoals:

15. a1: {p:(TT)| R1(1of(p),2of(p)) }
6. a2: {p:(TT)| R1(1of(p),2of(p)) }
7. a1 = a2 {p:(TT)| R2(1of(p),2of(p)) }
a1 = a2		1 step
 
25. a1: {p:(TT)| R1(1of(p),2of(p)) }
6. a2: {p:(TT)| R1(1of(p),2of(p)) }
a1 {p:(TT)| R2(1of(p),2of(p)) }		1 step
 
35. a1: {p:(TT)| R1(1of(p),2of(p)) }
6. a2: {p:(TT)| R1(1of(p),2of(p)) }
a2 {p:(TT)| R2(1of(p),2of(p)) }		1 step
 
45. b: {p:(TT)| R2(1of(p),2of(p)) }
a:{p:(TT)| R1(1of(p),2of(p)) }. a = b {p:(TT)| R2(1of(p),2of(p)) }		1 step

About:
productsetfunctionuniverseequalmemberpropallexists

(8steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc