(* percorsi di differenza etc. *)

open Lambda3;;

type formula =
  | Var of int
  | And of formula * formula
  | Or of formula * formula
;;

let rec mk_k_vars k =
  if k = 0 then []
  else `Var (k-1) :: (mk_k_vars (k-1))
;;

let is_lambda = function
  | `Lam _ -> true
  | _ -> false
;;

let rec diff k level t1 t2 =
  if is_lambda t1 || is_lambda t2
  then let vars = mk_k_vars k in
       let level = level + k in
       diff k level (mk_appl (lift k t1) vars) (mk_appl (lift k t2) vars)
  else assert false
;;