(6steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc

At: equivalence properties 1
1. T: Type
2. f: TT
3. x:T. f(x,x)
4. x,y:T. f(x,y) f(y,x)
5. x,y,z:T. f(x,y) f(y,z) f(x,z)
6. x: T
7. y: T
8. z: T
9. f(x,y)
10. f(y,z)

f(x,z)
By:
Witness5 x
THEN
With y (Analyze -1)
THEN
With z (Analyze -1)
Generated subgoal:

15. x: T
6. y: T
7. z: T
8. f(x,y)
9. f(y,z)
10. f(x,y) f(y,z) f(x,z)
f(x,z)

About:
boolassertapplyfunctionuniverseimpliesall

(6steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc