1 (* percorsi di differenza etc. *)
\r
7 | And of formula * formula
\r
8 | Or of formula * formula
\r
11 let rec mk_k_vars k =
\r
13 else `Var (k-1) :: (mk_k_vars (k-1))
\r
16 let is_lambda = function
\r
21 let rec diff k level t1 t2 =
\r
22 if is_lambda t1 || is_lambda t2
\r
23 then let vars = mk_k_vars k in
\r
24 let level = level + k in
\r
25 diff k level (mk_appl (lift k t1) vars) (mk_appl (lift k t2) vars)
\r