1	import Base
2	import ./proof.bend as P
3	import ../../../src/containers/stack.bend as D
4	import ../../../spec/containers/stack.bend as S
5	import ../../../src/containers/types/stack.bend as E
6	
7	def step_u32(+xs: List<&2, U32>, +op: E.Op<U32>) -> {D.step(~U32, P.real(~U32, xs), op) == P.lift(~U32, S.step(U32, xs, op)) : D.Stack<U32> & E.Obs<U32>}:
8	  P.step_correct(~U32, xs, op)
9	
10	def step_string(+xs: List<&2, String>, +op: E.Op<String>) -> {D.step(~String, P.real(~String, xs), op) == P.lift(~String, S.step(String, xs, op)) : D.Stack<String> & E.Obs<String>}:
11	  P.step_correct(~String, xs, op)
12	
13	def new_u32() -> {D.new(~U32) == P.real(~U32, Nil{}) : D.Stack<U32>}:
14	  P.constructor(~U32)
15	
16	def new_string() -> {D.new(~String) == P.real(~String, Nil{}) : D.Stack<String>}:
17	  P.constructor(~String)