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)