proposition: Lemma instanciated_active_subterm : forall s t sigma, active_subterm s t -> active_subterm (apply_subst sigma s) (apply_subst sigma t).
proof: Proof. intros s t sigma H; inversion H as [u | s' t' H']; clear H. left. subst; rewrite trans_clos_trans_clos_alt in H'; induction H' as [x y | x y z]. right; left. destruct y as [v | f l]. contradiction. destruct H as [i [H1 H2]]. exists i; split; trivial. generalize (nth_error_map (apply_subst sigma) l i); rewrite H2. case (nth_error (map (apply_subst sigma) l) i). intros ti Hi; rewrite Hi; apply eq_refl. contradiction. apply refl_trans_clos_is_trans with (apply_subst sigma y); trivial. right; left; destruct z as [v | f l]. contradiction. destruct H as [i [H1 H2]]. exists i; split; trivial. generalize (nth_error_map (apply_subst sigma) l i); rewrite H2. case (nth_error (map (apply_subst sigma) l) i). intros ti Hi; rewrite Hi; apply eq_refl. contradiction. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)