proposition: Lemma mark_inject_subst : forall t sigma, is_fapp t -> mark_term (inject_term (T.apply_subst sigma t)) = M.apply_subst (sigma_inject sigma) (mark_term (inject_term t)).
proof: Proof. intros; destruct t; [ contradiction H | clear H ]. simpl; f_equal; induction l; [ reflexivity |]; simpl; f_equal; [ apply inject_subst | assumption ]. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)