fact: Fixpoint enumerate {A} (ls : list A) (start : nat) : list (nat * A) := match ls with | nil => nil | x::xs => (start, x)::enumerate xs (S start) end.
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality