obj RecDB =  Rec*
    ops: Enter(RecDB, Rec)->RecDB;
	 Find(RecDB, Name)->Rec;
end;

obj Rec =  Name and Addr
    ops: Enter(RecDB, Rec)->RecDB;
	 Find(RecDB, Name)->Rec;
end;

obj Rec1 < Rec =  OneA and OneB;
obj Rec2 < Rec =  TwoA and TwoB;
obj Rec3 < Rec =  ThreeA and ThreeB;

op Enter(rdb:RecDB, r:Rec)->(rdb':RecDB)
    post: r in rdb';
end;

(*
 * Is it possible to auto-gen the following op, including the Rec(r1) upcast in
 * the postcond?
 *)
op Enter(rdb:RecDB, r:Rec1)->rdb':RecDB
    post: Rec(r) in rdb';
end;

op Enter(RecDB, Rec2);
op Enter(RecDB, Rec3);