proposition: Lemma undef_vars_app : forall (e1 e2 : expr) (l u1 u2 : prt_names), undef_vars e1 l u1 -> undef_vars e2 l u2 -> undef_vars (APP e1 e2) l (u1 ++ u2).
proof: Proof. split; intros. inversion_clear H. inversion_clear H0. red in |- *; simpl in |- *; intros. elim In_app with name x u1 u2; intros; auto with coc core arith datatypes. apply H1 with x; auto with coc core arith datatypes. apply H with x; auto with coc core arith datatypes. inversion_clear H. inversion_clear H0. elim In_app with name x u1 u2; intros; auto with coc core arith datatypes. Qed.
imports: MyList Termes Names