proposition: Theorem subst_comp_is_subst_comp : forall sigma1 sigma2 t, apply_subst (subst_comp sigma1 sigma2) t = apply_subst sigma1 (apply_subst sigma2 t).
proof: Proof. intros sigma1 sigma2 t; pattern t; apply term_rec3; clear t. intro v; unfold subst_comp; simpl; rewrite subst_comp_is_subst_comp_aux2; do 2 rewrite subst_comp_is_subst_comp_aux1; destruct (find eq_var_bool v sigma2); trivial; simpl; destruct (find eq_var_bool v sigma1); trivial. intros f l IH; simpl; apply (f_equal (fun l => Term f l)); induction l as [ | a l]; trivial. simpl; rewrite (IH a). rewrite IHl; trivial. intros; apply IH; right; trivial. left; trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)