% @(#)$Id: SortNames.proof,v 1.2 1997/02/13 00:21:13 leavens Exp $
set script SortNames
set log SortNames

%%% Proof Obligations for trait SortNames

execute SortNames_Axioms

%% Implications

declare variables
  s: S
  s1: S
  ..


% main trait: SortNames

set name SortNamesTheorem

prove
  (sort_of(s)) = (sort_of(s1))
  ..
   [] conjecture
qed