proposition: Lemma equiv_free_db : forall (l : prt_names) (t : term) (e : expr), term_expr_equiv l t e -> free_db (length l) t.
proof: Proof. simple induction 1; simpl in |- *; intros; auto with coc core arith datatypes. apply db_ref. elim H0; simpl in |- *; auto with coc core arith datatypes. Qed.
imports: MyList Termes Names