Substitution

let rec substitue f x g =
  match f with
  | Var i -> if i = x then g else Var i
  | Non h -> Non (substitue h x g)
  | Et (a, b) -> Et (substitue a x g, substitue b x g)
  | Ou (a, b) -> Ou (substitue a x g, substitue b x g)

Récursion sur la structure : on descend dans la formule et l'on remplace les feuilles Var x par g, en reconstruisant un nouvel arbre (les formules sont immuables). La substitution est l'opération de base de la réécriture de formules.