proposition: Lemma in_seq_image (n p : A) : List.In p (f_sequence n) -> exists k, f k = Some p.
proof: Proof. funelim (f_sequence n);[ | now intros abs; elim abs]. now simpl; intros [p_is_a | p_in_seq];[rewrite <- p_is_a; exists n | auto]. Qed.
imports: Program Bvector List Relations Equations(Equations Signature) Utf8 Arith Wf_nat Bvector Examples.Fin