proposition: Theorem nocc_Cons : forall (n m : nat) (x y : list nat), nocc n x = nocc n y -> nocc n (Cons nat m x) = nocc n (Cons nat m y).
proof: Proof. intros. unfold nocc in |- *. apply si_intro. intro. rewrite H0. simpl in |- *. apply eq_S. assumption. intro. rewrite H0. simpl in |- *. assumption. Qed.