proposition: Lemma remove_several_subterms_bis_nil : forall sigma f v v' t l2, arity f = AC -> well_formed_cf_subst sigma -> well_formed_cf (Term f l2) -> apply_cf_subst sigma (Var v) = Term f (quicksort (flatten f (apply_cf_subst sigma (Var v') :: t :: nil))) -> apply_cf_subst sigma (Var v) = Term f l2 -> match t with | Var _ => True | Term g _ => f<>g end -> match remove T.eq_bool t l2 with | None => False | Some l3 => apply_cf_subst sigma (Var v') = build f l3 end.
proof: Proof. intros sigma f v v' t l2 Ar W_sigma Wt2 v_sigma t1_sigma Al_t; 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]]]]]. injection l2'''_eq; clear l2'''_eq; intro l2'''_eq; subst l2 l2'''; apply flatten_cf with f; trivial. apply well_formed_cf_apply_subst; trivial; simpl; trivial. apply well_formed_cf_build_inside with t; subst; trivial. apply permut_trans with (l2' ++ l2''). rewrite (@permut_cons t t). apply permut_trans with (l2' ++ t :: l2''). assert (H:= trans_eq (sym_eq v_sigma) t1_sigma). assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l''). intros l' l'' H''; injection H''; intros; subst; trivial. subst cp1; rewrite <- (Inj _ _ H); clear Inj. apply permut_sym; apply quick_permut_bis. apply permut_trans with (flatten f (apply_cf_subst sigma (Var v') :: nil) ++ flatten f (t :: nil)). rewrite <- flatten_app; simpl app; apply permut_refl. refine (permut_trans (list_permut_app_app _ _) _). simpl; destruct t as [ x | g ll ]; [apply permut_refl | idtac]. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g; absurd (f = g); trivial | intros _; reflexivity]. apply permut_sym; rewrite <- permut_cons_inside; reflexivity. reflexivity. apply permut_sym; apply flatten_build_inside with t; subst cp1; trivial. intros Not_in; apply Not_in. assert (H := trans_eq (sym_eq v_sigma) t1_sigma). assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l''). intros l' l'' H'; injection H'; intros; subst; trivial. rewrite <- (Inj _ _ H); clear Inj. apply in_impl_mem. reflexivity. rewrite <- in_quick_in. assert (H':= flatten_app f (apply_cf_subst sigma (Var v') :: nil) (t :: nil)). simpl in H'; simpl; rewrite H'; apply in_or_app; right. destruct t as [ x | g ll ]; simpl; [left; trivial | idtac]. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g; absurd (f = g); trivial | intros _; left; reflexivity]. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac matching_sound)