(14steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc

At: discrete equality unique 1 1 1 1 1 1
1. T: Type
2. f1: TT
3. f1 TT
4. f2: TT
5. x,y:T. f2(x,y) x = y
6. f2 TT
7. v: T
8. w: T
9. b1:
10. f1(v,w) = b1
11. b2:
12. f2(v,w) = b2
13. f1(v,w) v = w

b1 = b2
By:
Witness5 v
THEN
With w (Analyze -1)
Generated subgoal:

15. f2 TT
6. v: T
7. w: T
8. b1:
9. f1(v,w) = b1
10. b2:
11. f2(v,w) = b2
12. f1(v,w) v = w
13. f2(v,w) v = w
b1 = b2

About:
boolassertapplyfunctionuniverseequalmemberall

(14steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc