Require Export SM2.


Section SM2well_formed_V_def.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { sm_context       : SMcontext }.
  Context { sm_auth          : SMauth }.
  Context { sm_initial_keys  : SMinitial_keys }.



  Definition entries_have_different_values
             (v1 v2 : sm_values) : Prop :=  v1 <> v2.

  Inductive well_formed_V : sm_values -> Prop :=
  | well_formed_V_nil : well_formed_V []
  | well_formed_V_cons :
      forall val L,
        (forall val',
            In val' L
            -> val <> val')
        -> well_formed_V L
        -> well_formed_V (val :: L).
  Hint Constructors well_formed_V.

End SM2well_formed_V_def.


Hint Constructors well_formed_V.
