Implication et contraposée

let implique a b = Ou (Non a, b)

let f = implique (Var 0) (Var 1)                       (* x0 => x1 *)
let g = implique (Non (Var 1)) (Non (Var 0))           (* (non x1) => (non x0) *)
(* equivalentes f g  vaut  true *)

On construit les deux formules avec implique, puis equivalentes f g confirme par énumération qu'elles ont la même table de vérité : une implication équivaut toujours à sa contraposée. Représenter les connecteurs dérivés (=>, <->) par des combinaisons des trois de base est une technique récurrente.