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

At: discrete equality unique 1 1 1 1 1 1 1
1. T: Type
2. f1: TT
3. f1 TT
4. f2: TT
5. 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
By: HypSubst -3 -1
Generated subgoal:

113. b2 v = w
b1 = b2

About:
boolassertapplyfunctionuniverseequalmember

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