proposition: Lemma inject_subst : forall t sigma, inject_term (T.apply_subst sigma t) = M.apply_subst (sigma_inject sigma) (inject_term t).
proof: Proof. intros; pattern t; apply T.term_rec3; intros. induction sigma as [|[v0 t0] sigma]; [ reflexivity |]; simpl; case (M.eq_var_bool v v0); [ reflexivity | assumption ]. simpl; f_equal; revert H; induction l; simpl; intros; [ reflexivity | f_equal; [ apply H; left; reflexivity |]]; apply IHl; intros; apply H; right; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)