Require Export PBFTtactics3.
Require Export PBFTcollision_resistant.


Section PBFT_A_1_9_misc5.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { pbft_context     : PBFTcontext      }.
  Context { pbft_auth        : PBFTauth         }.
  Context { pbft_keys        : PBFTinitial_keys }.
  Context { pbft_hash        : PBFThash         }.
  Context { pbft_hash_axioms : PBFThash_axioms  }.


  Lemma eq_digests_implies_eq_requests :
    forall rs rs',
      requests2digest rs = requests2digest rs'
      -> rs = rs'.
  Proof.
    introv eqrs.
    unfold requests2digest in *.
    apply create_hash_messages_collision_resistant in eqrs.
    revert dependent rs'.
    induction rs; introv eqrs;
      repeat (simpl in *; ginv; smash_pbft; tcsp);
      destruct rs'; simpl in *; smash_pbft.
    inversion eqrs; subst; f_equal; tcsp.
  Qed.

End PBFT_A_1_9_misc5.
