proposition: Lemma indexes_interval l : indexes l = interval 0 (length l).
proof: Proof. set (P := fun start (l indexesl : list nat) => indexesl = interval start (length l)). revert l. apply (indexes_elim (P 0) (fun l acc n indexesl => n <= length l -> P n l acc -> P 0 l indexesl)); subst P; simpl. intros l. + intros H. apply H; auto. rewrite interval_large; trivial; lia. + intros; trivial. + intros l ? n H Hn ->. apply H. lia. rewrite (interval_equation_1 n). destruct lt_dec. reflexivity. elim n0. lia. Qed.
imports: Equations(Equations) Coq(List Program.Syntax Arith Lia)