A manual proof of discrimination
Prove manually (i.e without Discriminate)
the inequality true<>false.
The definition of the local function is_true is a beautiful
illustration of the relationship between bool and Prop.
Notice the use of change, which illustrates the importance
of type conversion.