let rec apply rho q =
  match q with
    | Var(x) -> 
        (try
           List.assoc x rho
         with
             Not_found -> q)
    | (True | False | Atom _) -> q
    | Disj(ql) ->
        mk_disj (List.map (apply rho) ql)
    | Iff(q1, q2) -> 
        mk_iff (apply rho q1) (apply rho q2)
    | Ite(q1, q2, q3) -> 
        mk_ite (apply rho q1) (apply rho q2) (apply rho q3)
    | Neg(q1) ->
        mk_neg (apply rho q1)
    | Let(x, q1, q2) -> 
        apply ((x, q1) :: rho) q2