proposition: Lemma in_elt_inv : forall (x y : A) l1 l2, In x (l1 ++ y :: l2) -> x = y \/ In x (l1 ++ l2).
proof: Proof. intros x y l1 l2 Hin. apply in_app_or in Hin. destruct Hin as [Hin|[Hin|Hin]]; [right|left|right]; try apply in_or_app; intuition. Qed.
imports: PeanoNat