% @(#)$Id: WidenNarrow.proof,v 1.2 1997/02/13 00:21:25 leavens Exp $

set script WidenNarrow
set log WidenNarrow

%%% Proof Obligations for trait WidenNarrow

execute WidenNarrow_Axioms

%% Implications

declare variables
  u: Untyped
  ..


% main trait: WidenNarrow

set name WidenNarrowTheorem

prove
  (narrow(widen(narrow(u)))) = (narrow(u))
  ..
  [] conjecture
qed