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

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

f1(v) = f2(v)
By: ExtWith [`w'] [T]
Generated subgoal:

19. w: T
f1(v,w) = f2(v,w)

About:
boolassertapplyfunctionuniverseequalmemberall

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