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

At: discrete equality unique 1 1 1 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. f1(v,w) = true
9. f2(v,w) = false
10. True v = w
11. True (v = w)
12. False v = w
13. False (v = w)

true = false
By: Analyze 10
Generated subgoal:

110. True (v = w)
11. False v = w
12. False (v = w)
13. v = w
true = false

About:
boolbfalsebtrueapplyfunctionuniverseequalmemberimpliesfalsetrue

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