proposition: Theorem nocc_ins : forall (x : list nat) (n m : nat), nocc n (ins m x) = nocc n (Cons nat m x).
proof: Proof. simple induction x. trivial. intros. rewrite ins_eq2. apply (si_intro (list nat) (fun t : list nat => nocc n t = nocc n (Cons nat m (Cons nat x0 l)))). trivial. intro. rewrite nocc_Cons_Cons. apply nocc_Cons. apply H. Qed.