fact: Definition level (s t : stack A) : stack A * stack A := match Nat.compare (length s) (length t) with | Lt => (s , truncate (length s) t) | Eq => (s, t) | Gt => (truncate (length t) s, t) end.
imports: Coq(List) Coq(Arith)