proposition: Lemma incl_app_sym : forall l1 l2 : List, incl (l1 ++ l2) (l2 ++ l1).
proof: Proof. red in |- *; intros. elim In_app with x l1 l2; intros; auto with coc core arith datatypes. elim l2; simpl in |- *; auto with coc core arith datatypes. elim H0; simpl in |- *; auto with coc core arith datatypes. Qed.
imports: Le Gt List