proposition: Lemma add_new_var_to_subst : forall t1 v t2 sigma, ~occurs_in_term v t1 -> apply_cf_subst sigma t1 = apply_cf_subst ((v,t2) :: sigma) t1.
proof: Proof. intro t1; pattern t1; apply term_rec3; clear t1. intros v v0 t2 sigma O; simpl; generalize (X.eq_bool_ok v v0); case (X.eq_bool v v0); [intro v_eq_v0; subst v | intros _]. apply False_rect; apply O; unfold occurs_in_term; trivial. reflexivity. intros f l IH v t2 sigma O; simpl. assert (H : map (apply_cf_subst sigma) l = map (apply_cf_subst ((v,t2) :: sigma)) l). induction l as [ | t l]. trivial. simpl map; rewrite <- (IH t). rewrite <- IHl. reflexivity. intros; apply IH; [right | idtac]; assumption. intro v_in_l; apply O; right; assumption. left; reflexivity. intro v_in_t; apply O; left; assumption. rewrite H; reflexivity. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)