proposition: Lemma active_position_in_instanciated_term : forall p t s sigma, active_position (apply_subst sigma t) p = true -> subterm_at_pos t p = Some s -> active_position t p = true.
proof: Proof. intro p; induction p as [ | i p]. intros; trivial. intros [v | f l] s sigma; simpl. intros; discriminate. case (mem_bool Nat.eqb i (mu f)); [idtac | intros; discriminate]. generalize (nth_error_map (apply_subst sigma) l i). case (nth_error (map (apply_subst sigma) l) i); [idtac | intros; discriminate]; simpl. generalize (nth_error_ok_in i l); case (nth_error l i); [idtac | contradiction]. intros t H s' H'; destruct (H _ (eq_refl _)) as [l1 [l2 [L K]]]; clear H; subst. apply IHp; apply in_or_app; right; left; apply eq_refl. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)