let rec contains_var x t =
match t with
| Var v -> x == v
| Lam (a, b) -> contains_var x b
| App (a, b) -> contains_var x a || contains_var x b
| Flip (p, a, b) -> contains_var x a || contains_var x b
| Const _ -> false
| Case branches -> exists (contains_var x) (map snd branches)