proposition: Lemma In_app : forall (x : A) (l1 l2 : List), In x (l1 ++ l2) -> In x l1 \/ In x l2.
proof: Proof. simple induction l1; simpl in |- *; intros; auto with coc core arith datatypes. inversion_clear H0; auto with coc core arith datatypes. elim H with l2; auto with coc core arith datatypes. Qed.
imports: Le Gt List