proposition: Lemma equiv_unique : forall (l : prt_names) (t : term) (e : expr), term_expr_equiv l t e -> forall u : term, term_expr_equiv l u e -> t = u.
proof: Proof. simple induction 1; intros. inversion_clear H0; auto with coc core arith datatypes. inversion_clear H1. elim first_item_unique with name x l0 n n0; auto with coc core arith datatypes. inversion_clear H4. elim H1 with A0; auto with coc core arith datatypes. elim H3 with M0; auto with coc core arith datatypes. inversion_clear H4. elim H1 with u1; auto with coc core arith datatypes. elim H3 with v0; auto with coc core arith datatypes. inversion_clear H4. elim H1 with A0; auto with coc core arith datatypes. elim H3 with M0; auto with coc core arith datatypes. Qed.
imports: MyList Termes Names