CoinFormalizer

Right now instructions are typed against a stack, while programs are not: `Inductive has_prog_type : program -> instr_type -> Prop := ` `with has_instr_type : instr -> stack -> instr_type...

Right now stack type is defined as `with stack_type := | empty_stack : stack_type | cons_stack : type -> stack_type -> stack_type ` but it should be something as close...