proposition: Lemma occur_S : forall x l n, occur x l = S n -> exists m, exists p, l = m ++ x :: p /\ ~In x m /\ occur x p = n.
proof: Proof. intros. assert (occur x l > 0). lia. ded (occur_in H0). ded (in_elim_dec eq_dec H1). do 3 destruct H2. subst l. exists x0. exists x1. split. refl. split. exact H3. rewrite occur_app in H. simpl in H. rewrite eq_delta in H. ded (notin_occur H3). lia. Qed.
imports: CoLoR(ListUtil NatUtil LogicUtil)