proposition: Lemma inlist_head_neq : forall (A : Set) (x y : A) (l : list A), x <> y -> (inlist A x (Cons A y l) <-> inlist A x l).
proof: Proof. intros. unfold inlist in |- *. simpl in |- *. split. intros. elim H0. intro. elim H. assumption. intros. assumption. intros. right. assumption. Qed.
imports: Arith ZArith EqNat dec natZ