proposition: Lemma empty_subst_is_id : forall t, apply_subst nil t = t.
proof: Proof. intro t; pattern t; apply term_rec3; clear t; trivial. intros f l IH; simpl; apply (f_equal (fun l => Term f l)); induction l as [ | t l]; trivial; simpl; rewrite (IH t). rewrite IHl; trivial. intros; apply IH; right; trivial. left; trivial. Qed.
imports: List more_list list_permut list_set Arith