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

At: discrete equality unique 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

f1(v,w) = f2(v,w)
By:
GenConcl (f1(v,w) = b1)
THEN
GenConcl (f2(v,w) = b2)
Generated subgoal:

110. b1:
11. f1(v,w) = b1
12. b2:
13. f2(v,w) = b2
b1 = b2

About:
boolassertapplyfunctionuniverseequalmemberall

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