proposition: Lemma unique_alpha : forall (l1 : prt_names) (t : term) (e : expr), term_expr_equiv l1 t e -> forall (l2 : prt_names) (f : expr), term_expr_equiv l2 t f -> alpha l1 e l2 f.
proof: Proof. simple induction 1; intros. inversion_clear H0. apply alp_srt. inversion_clear H1. apply alp_ref. generalize l2 H2. elim H0; intros. inversion_clear H1. apply tr_hd. inversion_clear H5. apply tr_tl; auto with coc core arith datatypes. inversion_clear H4. apply alp_abs; auto with coc core arith datatypes. inversion_clear H4. apply alp_app; auto with coc core arith datatypes. inversion_clear H4. apply alp_prod; auto with coc core arith datatypes. Qed.
imports: MyList Termes Names