Require Export PBFTtactics2.



Ltac prove_by_ind2 ind h eqst sop p m eqtrig trig tac1 tac2 :=
  start_ind ind;
  introv;
  intro_state h eqst;
  try unroll_state;
  try unroll_send;
  try fold (@DirectedMsgs _ _ _) in *;
  simpl in *;
  destruct_unrolled_state sop p;
  op_st_some m eqtrig;
  try (rewrite eqtrig in *; simpl in *);
  simplify_ind ind;
  unfold_update ind trig tac1 tac2;
  simpl in *; ginv; subst; tcsp;
  try tac1;
  try (first [conflicting_sends|tac2 ind]).
