proposition: Lemma subst_projection : forall sigma f l, projection (apply_subst sigma (Term f l)) = apply_subst sigma (projection (Term f l)).
proof: Proof. unfold projection; intros sigma f l; simpl. generalize (nth_error_map (apply_subst sigma) l (P f)). case (nth_error (map (apply_subst sigma) l) (P f)). intros ti_sigma. case (nth_error l (P f)). intros ti H; assumption. contradiction. case (nth_error l (P f)). contradiction. intros; apply eq_refl. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)