Nuprl - Proof: rel-graph functionality

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

T:Type, R1,R2:(TTProp). (x,y:T. R1(x,y) R2(x,y)) Graph(x,y:T. R1(x,y)) Graph(x,y:T. R2(x,y))

By: Auto THEN Unfolds [`graph-isomorphic`;`rel-graph`] 0 THEN Reduce 0 THEN InstConcl [Id;Id] THEN Reduce 0 THEN Try (BackThru Thm* Bij(T; T; Id))

Generated subgoals:

1 1. T: Type
2. R1: TTProp
3. R2: TTProp
4. x,y:T. R1(x,y) R2(x,y)
Id {p:(TT)| R1(1of(p),2of(p)) }{p:(TT)| R2(1of(p),2of(p)) } 1 step

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) 5 steps

3 1. T: Type
2. R1: TTProp
3. R2: TTProp
4. x,y:T. R1(x,y) R2(x,y)
(Id,Id) o Id = Id o Id {p:(TT)| R1(1of(p),2of(p)) }TT 1 step

About:

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

1	1. `T:` `Type` 2. `R1:` `TTProp` 3. `R2:` `TTProp` 4. `x,y:T. R1(x,y) R2(x,y)` `Id {p:(TT)\| R1(1of(p),2of(p)) }{p:(TT)\| R2(1of(p),2of(p)) }`	1 step

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)`	5 steps

3	1. `T:` `Type` 2. `R1:` `TTProp` 3. `R2:` `TTProp` 4. `x,y:T. R1(x,y) R2(x,y)` `(Id,Id) o Id = Id o Id {p:(TT)\| R1(1of(p),2of(p)) }TT`	1 step