library viewtest1

%% The theorem link is provable with global subsumption

spec sp1 =
  sort s
end

spec sp2 =
  sp1
then
 sort t
end

view v1 : sp1 to sp2 end