proposition: Lemma indexes_spec (l : list nat) : Forall (fun x => x < length l) (indexes l).
proof: Proof. apply (indexes_elim (fun l indexesl => Forall (fun x => x < length l) indexesl) (fun l acc n indexesl => n <= length l -> Forall (fun x => x < length l) acc -> Forall (fun x => x < length l) indexesl)); clear l; intros. + apply H; constructor. + apply H0. + apply H. lia. constructor. lia. apply H1. Qed.
imports: Equations(Equations) Coq(List Program.Syntax Arith Lia)