proposition: Lemma equiv_no_undef : forall (l : prt_names) (t : term) (e : expr), term_expr_equiv l t e -> forall undef : prt_names, undef_vars e l undef -> undef = nil.
proof: Proof. simple induction 1; simple destruct undef; intros; auto with coc core arith datatypes. inversion_clear H0. cut (expr_vars n (SRT s)); intros; auto with coc core arith datatypes. inversion_clear H0. inversion_clear H1. elim H2 with n0; auto with coc core arith datatypes. cut (expr_vars n0 (REF x)); intros; auto with coc core arith datatypes. inversion_clear H1. elim H0; auto with coc core arith datatypes. inversion_clear H4. cut (expr_vars n (ABS x B N)); intros; auto with coc core arith datatypes. cut (n :: nil = nil); intros. discriminate H7. inversion_clear H4. apply H1. split; intros. red in |- *; simpl in |- *; intros. elim H5 with n; auto with coc core arith datatypes. generalize H4. inversion_clear H8; auto with coc core arith datatypes. inversion H9. generalize H7. inversion_clear H4; auto with coc core arith datatypes. inversion H8. apply H3. split; intros. red in |- *; simpl in |- *; intros. inversion H4. apply H7. elim H11. inversion_clear H9; auto with coc core arith datatypes. inversion H10. elim H5 with x0; auto with coc core arith datatypes. inversion_clear H9; auto with coc core arith datatypes. inversion H13. generalize H8. inversion_clear H4; auto with coc core arith datatypes. inversion H9. inversion_clear H4. cut (expr_vars n (APP a b)); intros; auto with coc core arith datatypes. cut (n :: nil = nil); intros. discriminate H7. inversion_clear H4. apply H1. split; intros. red in |- *; simpl in |- *; intros. elim H5 with n; auto with coc core arith datatypes. generalize H4. inversion_clear H8; auto with coc core arith datatypes. inversion H9. generalize H7. inversion_clear H4; auto with coc core arith datatypes. inversion H8. apply H3. split; intros. red in |- *; simpl in |- *; intros. elim H5 with n; auto with coc core arith datatypes. generalize H4. inversion_clear H8; auto with coc core arith datatypes. inversion H9. generalize H7. inversion_clear H4; auto with coc core arith datatypes. inversion H8. inversion_clear H4. cut (expr_vars n (PROD x B N)); intros; auto with coc core arith datatypes. cut (n :: nil = nil); intros. discriminate H7. inversion_clear H4. apply H1. split; intros. red in |- *; simpl in |- *; intros. elim H5 with n; auto with coc core arith datatypes. generalize H4. inversion_clear H8; auto with coc core arith datatypes. inversion H9. generalize H7. inversion_clear H4; auto with coc core arith datatypes. inversion H8. apply H3. split; intros. red in |- *; simpl in |- *; intros. inversion H4. apply H7. elim H11. inversion_clear H9; auto with coc core arith datatypes. inversion H10. elim H5 with x0; auto with coc core arith datatypes. inversion_clear H9; auto with coc core arith datatypes. inversion H13. generalize H8. inversion_clear H4; auto with coc core arith datatypes. inversion H9. Qed.
imports: MyList Termes Names