let rec subst x s t =
match t with
| Var v -> if (x == v) then s else t
| Lam (a, b) -> Lam (a, subst x s b)
| App (a, b) -> App (subst x s a, subst x s b)
| Flip (p, a, b) -> Flip (p, subst x s a, subst x s b)
| Const _ -> t
| Case branches ->
let subst_in_branch (n, a) = (n, subst x s a) in
Case (map subst_in_branch branches)