proposition: Lemma incl_Add_inv a l u v : ~In a l -> incl (a::l) v -> Add a u v -> incl l u.
proof: Proof. intros Ha H AD y Hy. assert (Hy' : In y (a::u)). { rewrite <- (Add_in AD). apply H; simpl; auto. } destruct Hy'; [ subst; now elim Ha | trivial ]. Qed.
imports: PeanoNat