A manual proof of discrimination

Prove manually (i.e without discriminate) the inequality true <> false.

Solution

Note

The definition of the local function is_true illustrates the relationship between bool and Prop.
Notice the use of change, which is an application of the rule of conversion.