A manual proof of discrimination

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


This file


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