fact: Fixpoint insert_nat (s:Stack) (n:nat) (a:Atom) : option Stack := match n,s with | O, _ => Some (a:::s) | S n', x :: xs => do s' <- insert_nat xs n' a; Some (x :: s') | _, _ => None end.
imports: ZArith List MSetPositive