proposition: Lemma remove_a_subterm : forall sigma f v l1 t l2, arity f = AC -> well_formed_cf_subst sigma -> well_formed_cf (Term f (Var v :: l1)) -> well_formed_cf (Term f l2) -> apply_cf_subst sigma (Var v) = t -> apply_cf_subst sigma (Term f (Var v :: l1)) = Term f l2 -> match remove T.eq_bool t l2 with | None => match t with | Var _ => False | Term g _ => f=g end | Some rmv => apply_cf_subst sigma (build f l1) = build f rmv end.
proof: Proof. intros sigma f v l1 t l2 Ar W_sigma Wt1 Wt2 v_sigma t1_sigma. generalize (in_remove _ _ T.eq_bool_ok t l2); destruct (remove T.eq_bool t l2) as [l2''' | ]. intros [cp1 [l2' [l2'' [ H'' [l2_eq l2'''_eq]]]]]; subst cp1. injection l2'''_eq; clear l2'''_eq; intro; subst l2 l2'''; apply flatten_cf with f; trivial. apply well_formed_cf_apply_subst; trivial; apply well_formed_cf_build_cons with (Var v); trivial. apply well_formed_cf_build_inside with t; trivial. rewrite <- (flatten_apply_cf_subst sigma l1 Ar); rewrite (flatten_build (l2' ++ l2'') Ar). simpl in t1_sigma; rewrite Ar in t1_sigma; simpl in v_sigma; rewrite v_sigma in t1_sigma. injection t1_sigma; clear t1_sigma; intro t1_sigma. destruct t as [ x | g ll]. rewrite (@permut_cons_inside (Var x) (Var x)) by reflexivity. setoid_rewrite <- t1_sigma. apply permut_sym; apply quick_permut_bis; reflexivity. revert t1_sigma; generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g | intros _]. absurd (f=g); trivial. apply (well_formed_cf_alien Ar Wt2 (Term g ll)). apply in_or_app; right; left; trivial. intro t1_sigma; rewrite (@permut_cons_inside (Term g ll) (Term g ll)) by reflexivity. setoid_rewrite <- t1_sigma. apply permut_sym; apply quick_permut_bis; reflexivity. intros s s_in_l2'_l2''; destruct (in_app_or _ _ _ s_in_l2'_l2'') as [s_in_l2' | s_in_l2'']; apply (well_formed_cf_alien Ar Wt2); apply in_or_app; [left | right; right]; trivial. intros t_not_in_l2; simpl in t1_sigma; rewrite Ar in t1_sigma; simpl in v_sigma; rewrite v_sigma in t1_sigma; inversion t1_sigma. destruct t as [x | g ll]. apply t_not_in_l2; subst l2. rewrite <- (mem_permut_mem (Var x) (quick_permut (Var x :: flatten f (map (apply_cf_subst sigma) l1)))); left; trivial. reflexivity. revert H0; generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intros f_eq_g _; assumption | intros f_diff_g]. intro H; apply False_rect; apply t_not_in_l2; subst l2. rewrite <- (mem_permut_mem (Term g ll) (quick_permut (Term g ll :: flatten f (map (apply_cf_subst sigma) l1)))). left; reflexivity. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac matching_sound)