proposition: Lemma subst_replace_at_pos : forall t u p sigma, is_a_pos t p = true -> apply_subst sigma (replace_at_pos t u p) = replace_at_pos (apply_subst sigma t) (apply_subst sigma u) p.
proof: Proof. intros t u p; revert t u; induction p as [ | i p]; intros t u sigma Hpos; trivial. destruct t as [x | f l]. discriminate. rewrite replace_at_pos_unfold. simpl apply_subst. rewrite replace_at_pos_unfold. apply f_equal. simpl in Hpos. clear f. revert i u sigma Hpos; induction l as [ | t l]; intros [ | n] u sigma Hpos; simpl; trivial. apply (f_equal (fun t => t :: map (apply_subst sigma) l)). apply IHp; trivial. apply f_equal. apply IHl; trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)