proposition: Lemma Exists_app l1 l2 : Exists (l1 ++ l2) <-> Exists l1 \/ Exists l2.
proof: Proof. induction l1; simpl; split; intros HE; try now intuition. - inversion_clear HE; intuition. - destruct HE as [HE|HE]; intuition. inversion_clear HE; intuition. Qed.
imports: PeanoNat