let prop_sat s p =
  match Prop.sat s p with
    | None -> None
    | Some(rho, _) -> Some(rho)