Nuprl - Proof: fun-graph-rel-graph 3 1 1

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

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))
6. a3: A
7. a4: B
8. a5: A
9. a6: B
10. < a3,f(a3,a4) > = < a5,f(a5,a6) >
11. b:B. f(a3,a4) = f(a3,b)

< a3,a4 > = < a5,a6 >

By: SplitPair -2 THEN ExRepD THEN Analyze

Generated subgoal:

1 10. b: B
11. f(a3,a4) = f(a3,b)
12. a3 = a5
13. f(a3,a4) = f(a5,a6)
a4 = a6 2 steps

About:

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