type 'a prop =
  | Top 
  | Bot 
  | V of 'a 
  | Et of 'a prop * 'a prop 
  | Ou of 'a prop * 'a prop 
  | Non of 'a prop
  | Implique of 'a prop * 'a prop 
;;

let e  = Non (Ou (Et (V "a", V "b"), Et (V "a", V "c"))) ;;

let f1 = Implique (Et (V "c", Non (V "a")), Ou (V "b", Implique (V "c", V "a"))) ;;

let f2 = Ou (Implique (V "b", Implique (V "c", V "a")), Ou (Non (V "c"), V "a")) ;;

let f3 =
  Ou (Et (V "a", V "b"),
      Ou (V "c",
          Ou (Non (Et (V "b", Non (V "c"))), Ou (Non (V "a"), Non (V "c")))))
;;

let f4=
  Ou (Et (V "a", V "b"),
      Ou (V "c",
          Ou (Et (Non (V "b"), Non (V "c")), Ou (Non (V "a"), Non (V "c"))))) ;;

let f5 =
  Ou (V "a",
      Ou (Et (Non (V "b"), Non (V "c")),
          Ou (Et (Non (V "a"), V "c"), Et (V "b", Non (V "c")))))
;;

(* pour plus tard *)
exception Contre_ex of (string * bool) list ;;

(* pour la fin *)

type 'a arbre_quine =
  | Valide
  | Invalide
  | Branchement of 'a * 'a arbre_quine * 'a arbre_quine
;;