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

At: fun-graph-rel-graph 3 1 1 1
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. b: B
11. f(a3,a4) = f(a3,b)
12. a3 = a5
13. f(a3,a4) = f(a5,a6)
a4 = a6
By: HypSubst -2 -1
Generated subgoal:

113. f(a5,a4) = f(a5,a6)
a4 = a6		1 step

About:
decidablefunctionuniverseequalimpliesallexists

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