Inductive term : Set :=
    nil : term
  | s : term -> term
  | __aux__vars8 : term -> term -> term
  | __aux__vars9 : term -> term -> term -> term -> term -> term
  | __aux__vars10 : term -> term -> term -> term
  | __aux__vars2 : term -> term -> term
  | current_session : term -> term -> term -> term
  | intruder : term
  | cons : term -> term -> term
  | __aux__vars4 : term -> term -> term
  | prv : term
  | pub : term
  | __aux__vars11 : term -> term -> term
  | __aux__vars5 : term -> term
  | __aux__vars7 : term -> term -> term -> term
  | key : term -> term -> term
  | bob : term
  | crypt : term -> term -> term
  | server : term
  | nonceb : term -> term -> term -> term
  | __aux__vars1 : term -> term
  | sym : term
  | alice : term
  | __aux__vars3 : term -> term
  | old_session : term -> term -> term -> term
  | noncea : term -> term
  | __aux__vars6 : term -> term -> term
.
