fact: Fixpoint nth'_helper {A} (n : nat) (ls : list A) (default : A) (offset : nat) := match ls with | nil => default | x::xs => if Nat.eqb n offset then x else nth'_helper n xs default (S offset) end.
imports: Coq.Lists.List Fiat.Common.BoolFacts Fiat.Common.Equality