proposition: Lemma undef_vars_incl : forall (e : expr) (l u1 u2 : prt_names), incl _ u1 u2 -> undef_vars e l u2 -> undef_vars e l u1.
proof: Proof. unfold undef_vars in |- *; split. inversion_clear H0. red in |- *; simpl in |- *; intros. apply H1 with x; auto with coc core arith datatypes. inversion_clear H0; auto with coc core arith datatypes. Qed.
imports: MyList Termes Names