Nuprl - Proof: fun-graph-rel-graph 4

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

At: fun-graph-rel-graph 4

1. A: Type
2. B: Type
3. f: ABA
4. a:A, b1,b2:B. f(a,b1) = f(a,b2) b1 = b2
5. a,a':A. Dec(b:B. a' = f(a,b))

(Id,Id) o p. < 1of(p),f(1of(p),2of(p)) > = Id o (p. < 1of(p),f(1of(p),2of(p)) > ) ABAA

By: GenConcl ((p. < 1of(p),f(1of(p),2of(p)) > ) = g) THEN RWO Thm* g:(ABC). (Id,Id) o g = g 0 THEN RWO Thm* f:(AB). Id o f = f 0

Generated subgoals:

None

About:

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