Goal:
    G : t  HI : invariants  x : Nbar.t  y : Nbar.t
  ============================
   ((Some 0 <= x)%nbar ->
    to_label (max x y) = Nat.max (to_label x) (to_label y))


DEBUG:Going to execute:
destruct x; intros H; simpl in H