goto : {l1 l2 : Level} {I : Set l1} {O : Set l2}
   !$\rightarrow$! CodeSegment I O !$\rightarrow$! I !$\rightarrow$! O
goto (cs b) i = b i