proposition: Lemma In_list_size: forall x xs, In x xs -> f x < S (list_size xs).
proof: Proof. intros. funelim (list_size xs); simpl in *. destruct H. destruct H0. * subst; lia. * specialize (H _ H0). intuition. lia. Qed.
imports: Program Equations(Equations) Utf8 Lia Arith List