fact: Definition conv_for_stack (v : Value) : Value := match v with | Num (B b) => Num (I (b2i b)) | Num (Sh s) => Num (I (s2i s)) | _ => v end.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)