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

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

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

13. 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

About:
boolassertapplyfunctionuniverseequalmemberall

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