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

At: discrete equality unique 1 1 1 1 1 1 1 1 1 2
1. T: Type
2. f1: TT
3. f1 TT
4. f2: TT
5. f2 TT
6. v: T
7. w: T
8. f1(v,w) = false
9. f2(v,w) = true
10. False v = w
11. False (v = w)
12. True v = w
13. True (v = w)

false = true
By: Analyze 12
Generated subgoal:

112. True (v = w)
13. v = w
false = true

About:
boolbfalsebtrueapplyfunctionuniverseequalmemberimpliesfalsetrue

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