A manual proof of discrimination

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

Solution

This file

Note

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.



Going home
Pierre Castéran