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