let a = App (Abs ("x", App (Var "x", Var "x")),
App (Abs ("x", App (Var "x", Var "x")), Var "x"));;

let y = Abs ("f", App (Abs ("x", App (Var ("f"), (App (Var ("x"), Var ("x"))))),
Abs ("x", App (Var ("f"), (App (Var ("x"), Var ("x")))))));;

let b = Abs ("w", App (App (Var "x", Abs ("y", App (App (Var "x", Abs ("x", Var "x")), Var "y"))), Abs ("t", Var "y")));;

let print_list = iter (print_string);;

let rec print_term t =
match t with
Var a -> a
|App (a, b) -> "(" ^ (print_term a) ^ " " ^ (print_term b) ^ ")"
|Abs (a, b) -> "\\" ^ a ^ "." ^ (print_term b);;

let isin l a = fold_left (fun x y -> (y = a) or x) false l;;

let unique z =
let rec unique' l acc =
match l with
[] -> acc
|l1::ls -> if isin acc l1 then (unique' ls acc) else (unique' ls (l1::acc))
in unique' z [];;

let fv z =
let rec fv' exp =
match exp with
Var a -> [a]
|App (a, b) -> (fv' a) @ (fv' b)
|Abs (a, b) -> filter (fun z -> (z <> a)) (fv' b)
in unique (fv' z);;

let cx y z =
let rec cx' a x =
if (not (isin (fv a) x)) then [] else (
match a with
Var b -> []
|App (b, c) -> (cx' b x) @ (cx' c x)
|Abs (b, c) -> (cx' c x) @ [b] )
in unique (cx' y z);;

print_list (cx y "x");;
print_string (print_term a);;