Require Export PBFTreceived_prepare_like1.



Hint Extern 1 =>
  match goal with
  | [ H : In (send_view_change _ _) (check_broadcast_prepare _ _ _) |- _ ] =>
    apply send_view_change_not_in_check_broadcast_prepare in H; destruct H
  end : pbft_false.


Hint Extern 1 =>
  match goal with
  | [ H : False |- _ ] => destruct H
  end : pbft_false.


Hint Extern 1 =>
  match goal with
  | [ H : In (send_view_change _ _) (check_broadcast_commit _ _ _) |- _ ] =>
    apply send_view_change_not_in_check_broadcast_commit in H; destruct H
  end : pbft_false.


Hint Extern 1 =>
  match goal with
  | [ H : check_send_replies _ _ _ _ _ _ = (?x, _), J : In (send_view_change _ _) ?x |- _ ] =>
    eapply message_in_check_send_replies_implies in H;[|exact J]; ginv
  end : pbft_false.
