proposition: Lemma empty_subst_is_id_list : forall l, map (apply_subst nil) l = l.
proof: Proof. intro l; induction l as [ | t l]; simpl; [idtac | rewrite empty_subst_is_id; rewrite IHl]; trivial. Qed.
imports: List more_list list_permut list_set Arith