# Some bad inference rules

Among many logical mistakes, we often meet bad inference rules, the use of
which can lead to inconsistencies.
For instance, let us consider implication dyslexia (confusion between
*P->Q* and *Q->P*) and dyslexic contraposition :
Definition dyslexic_imp := forall P Q:Prop, (P->Q)->Q->P.
Definition dyslexic_contrap :=forall P Q:Prop,(P->Q)->~P->~Q.

Show that if one or the other of the preceding types was inhabited,
one could prove `False`, hence any proposition.
## Solution

Look at file dyslexia.v

Going home

Pierre Castéran