proposition: Lemma decompose_subst : forall s sigma t tau, well_formed s -> (forall x u, In (x,u) sigma -> match u with | Var _ => True | Term f l => (match F.arity f with Free n => n | _ => 2 end) <> length l end) -> (forall x u v, In (x,u) sigma -> In (x,v) sigma -> u = v) -> (forall x y u, In (x,u) sigma -> In (y,u) sigma -> x = y) -> (forall x, In x (var_list s) <-> In x (map (@fst _ _) sigma)) -> well_formed t -> apply_subst tau t = apply_subst sigma s -> {phi : substitution | (forall v, In v (var_list t) -> apply_subst (subst_comp sigma phi) (Var v) = apply_subst tau (Var v)) /\ apply_subst phi t = s /\ (forall v, In v (map (@fst _ _) phi) <-> In v (var_list t)) /\ well_formed_subst phi}.
proof: Proof. intros s sigma t tau Ws H1 H2 H3 H4 Wt H0; assert (Aux : forall v p, subterm_at_pos t p = Some (Var v) -> {v_val : term | subterm_at_pos s p = Some v_val /\ apply_subst sigma v_val = apply_subst tau (Var v)}). revert sigma t tau Ws H1 H2 H3 H4 Wt H0. pattern s; apply term_rec3; clear s. intros v sigma t tau Ws H1 H2 H3 H4 Wt H0; simpl in H0; revert H0. assert (v_in_sig : In v (map (@fst _ _) sigma)). rewrite <- H4; left; apply eq_refl. destruct (mem_map_set _ _ X.eq_bool_ok (@fst _ _) v sigma) as [[v' v_val] [v_eq_v' v_in_sig']]. apply in_impl_mem; [reflexivity | assumption]. simpl in v_eq_v'; subst v'. rewrite (subst_aux _ H2 _ _ v_in_sig'). generalize (H1 _ _ v_in_sig'); destruct v_val as [x | f l]. intros _; destruct t as [y | ]; [idtac | intro; discriminate]. intros H0 x' [ | i p]; [idtac | intro; discriminate]. intro H; injection H; clear H; intro H; subst x'. exists (Var v); split. apply eq_refl. rewrite H0; simpl; rewrite (subst_aux _ H2 _ _ v_in_sig'); apply eq_refl. intros L; destruct t as [y | g k]. intros H0 x' [ | i p]; [idtac | intro; discriminate]. intro H; injection H; clear H; intro H; subst x'. exists (Var v); split. apply eq_refl. rewrite H0; simpl; rewrite (subst_aux _ H2 _ _ v_in_sig'); apply eq_refl. intro H0; injection H0; clear H0; do 2 intro; subst g l. apply False_rect; apply L; rewrite map_length; apply sym_eq. destruct (well_formed_unfold Wt) as [_ L']; destruct (F.arity f); assumption. intros f ls Hls sigma t tau Ws H1 H2 H3 H4 Wt. destruct t as [y | g lt]. intros H0 x' [ | i p]; [idtac | intro; discriminate]. intro H; injection H; clear H; intro H; subst x'. exists (Term f ls); split. apply eq_refl. apply sym_eq; assumption. intro H0; injection H0; clear H0; intros H0 H0'; subst g. intros x [ | i p] Sub. discriminate. simpl in Sub. generalize (nth_error_ok_in i lt). destruct (nth_error lt i) as [ti | ]; [intros H; destruct (H _ (eq_refl _)) as [lt1 [lt2 [L H']]]; clear H | discriminate]. rewrite H' in H0; rewrite map_app in H0. destruct (split_map_set _ _ _ _ (sym_eq H0)) as [ls1 [ls2 [h1 [h2 h3]]]]. destruct ls2 as [ | si ls2]. discriminate. assert (si_in_ls : In si ls). rewrite h1; apply in_or_app; right; left; apply eq_refl. destruct (Hls _ si_in_ls (subst_rest (var_list si) sigma) ti tau) with x p as [v_val [Sub' Sub'']]. destruct (well_formed_unfold Ws) as [Wls _]; apply Wls; trivial. intros y u yu_in_rest_sig; apply (H1 y); apply subst_rest_subst with (var_list si); trivial. intros y u v yu_in_rest_sig yv_in_rest_sig; apply (H2 y u v). apply (subst_rest_subst _ _ _ _ yu_in_rest_sig). apply (subst_rest_subst _ _ _ _ yv_in_rest_sig). intros y z u yu_in_rest_sig zu_in_rest_sig; apply (H3 y z u). apply (subst_rest_subst _ _ _ _ yu_in_rest_sig). apply (subst_rest_subst _ _ _ _ zu_in_rest_sig). intros y; split. intro y_in_si. assert (y_in_sig : In y (map (@fst _ _) sigma)). rewrite <- H4; rewrite h1. rewrite var_list_unfold; rewrite var_list_list_app; apply in_or_app; right; apply in_or_app; left; assumption. rewrite in_map_iff in y_in_sig; destruct y_in_sig as [[y' u] [y_eq_y' y_in_sig]]; simpl in y_eq_y'; subst y'. rewrite in_map_iff; exists (y,u); split; trivial. apply subst_rest_subst_rest; trivial. intro y_in_rest_subst; rewrite in_map_iff in y_in_rest_subst; destruct y_in_rest_subst as [[y' u] [y_eq_y' y_in_rest_subst]]; simpl in y_eq_y'; subst y'. apply subst_rest_rest with sigma u; trivial. destruct (well_formed_unfold Wt) as [Wlt _]; apply Wlt; rewrite H'; apply in_or_app; right; left; apply eq_refl. injection h3; clear h3; intros _ h3; rewrite <- h3. rewrite <- subst_eq_vars; intros z z_in_si; rewrite subst_rest_ok; trivial. assumption. exists v_val; split. simpl; rewrite h1; subst i; replace (length lt1) with (length ls1). rewrite nth_error_at_pos; assumption. rewrite <- (length_map (apply_subst sigma) ls1). rewrite <- (length_map (apply_subst tau) lt1). apply f_equal; assumption. rewrite <- Sub''; rewrite <- subst_eq_vars; intros v v_in_val. rewrite subst_rest_ok; trivial. apply var_in_subterm with v_val p; trivial. assert (Aux2 : forall v, mem (@eq _) v (var_list t) -> {v_val : term | apply_subst sigma v_val = apply_subst tau (Var v) /\ (forall p, subterm_at_pos t p = Some (Var v) -> subterm_at_pos s p = Some v_val) /\ well_formed v_val}). intros v v_in_t. destruct (var_in_subterm2 _ _ v_in_t) as [p Sub]. destruct (Aux v p Sub) as [v_val [Sub' H]]. exists v_val; split; trivial. split. intros q Subq. destruct (Aux _ _ Subq) as [v_val' [Sub'' H']]. rewrite Sub''; apply f_equal. apply decompose_subst_aux with sigma; trivial. apply (well_formed_subterm q Ws Sub''). apply (well_formed_subterm p Ws Sub'). intros x x_in_v_val'; rewrite <- H4. apply var_in_subterm with v_val' q; trivial. intros x x_in_v_val; rewrite <- H4. apply var_in_subterm with v_val p; trivial. rewrite H; assumption. apply (well_formed_subterm p Ws Sub'). clear Aux. revert Wt s Ws sigma tau H0 H1 H2 H3 H4 Aux2; pattern t; apply term_rec3; clear t. intros v _ s Ws sigma tau H0 H1 H2 H3 H4 Aux2. destruct (Aux2 v) as [v_val [K1 [K2 K3]]]. left; apply eq_refl. exists ((v,v_val) :: nil); split. intros z [z_eq_v | z_in_nil]; [subst z | contradiction]. rewrite subst_comp_is_subst_comp; simpl; rewrite eq_var_bool_refl; rewrite K1; trivial. split. simpl; simpl; rewrite eq_var_bool_refl. assert (K2' := K2 nil (eq_refl _)); injection K2'; intros; apply sym_eq; assumption. split. intros z; split; intro H; assumption. unfold well_formed_subst; simpl. intro z; generalize (X.eq_bool_ok z v); case (X.eq_bool z v); [intro z_eq_v | intro z_diff_v]; trivial. intros f lt Hlt Wt s Ws sigma tau H0 H1 H2 H3 H4 Aux2. destruct s as [x | g ls]. apply False_rect. destruct (well_formed_unfold Wt) as [_ L]. assert (x_in_sig : In x (map (@fst _ _) sigma)). rewrite <- H4; left; apply eq_refl. rewrite in_map_iff in x_in_sig; destruct x_in_sig as [[x' u] [x_eq_x' x_in_sig]]; simpl in x_eq_x'; subst x'. simpl in H0; rewrite (subst_aux _ H2 _ _ x_in_sig) in H0; subst u. apply (H1 _ _ x_in_sig); apply sym_eq; rewrite length_map; destruct (F.arity f); assumption. simpl in H0; injection H0; clear H0; intros H0 h0; subst g. rewrite var_list_unfold in *. destruct (well_formed_unfold Wt) as [Wlt _]; clear Wt. destruct (well_formed_unfold Ws) as [Wls _]; clear Ws. revert Wlt ls Wls sigma H0 H1 H2 H3 H4 Aux2; induction lt as [ | t lt]; intros Wlt ls Wls sigma H0 H1 H2 H3 H4 Aux2. destruct ls as [ | s ls]; [idtac | discriminate]. exists nil; repeat split. intros; contradiction. intro; assumption. intro; assumption. destruct ls as [ | s ls]; [discriminate | idtac]. injection H0; clear H0; intros H0 h0. destruct (Hlt t (or_introl _ (eq_refl _)) (Wlt t (or_introl _ (eq_refl _))) s (Wls s (or_introl _ (eq_refl _))) (subst_rest (var_list s) sigma)) with tau as [phi [k1 [k2 [k3 k4]]]]; trivial. rewrite h0; rewrite <- subst_eq_vars; intros x x_in_s; rewrite subst_rest_ok; trivial. intros x u xu_in_rest_sig; apply (H1 x u); apply subst_rest_subst with (var_list s); trivial. intros x u v xu_in_rest_sig xv_in_rest_sig; apply (H2 x u v); apply subst_rest_subst with (var_list s); trivial. intros x y u xu_in_rest_sig yu_in_rest_sig; apply (H3 x y u); apply subst_rest_subst with (var_list s); trivial. intro x; split. intro x_in_s; assert (x_in_sig : In x (map (@fst _ _) sigma)). rewrite <- H4; simpl; apply in_or_app; left; assumption. rewrite in_map_iff in x_in_sig; destruct x_in_sig as [[x' u] [x_eq_x' x_in_sig]]; simpl in x_eq_x'; subst x'. rewrite in_map_iff; exists (x,u); split; trivial. apply subst_rest_subst_rest; trivial. intro x_in_rest_sig; rewrite in_map_iff in x_in_rest_sig; destruct x_in_rest_sig as [[x' u] [x_eq_x' x_in_rest_sig]]; simpl in x_eq_x'; subst x'. apply subst_rest_rest with sigma u; trivial. intros v v_in_t; destruct (Aux2 v) as [v_val [K1 [K2 K3]]]. simpl; rewrite <- mem_or_app; left; assumption. exists v_val; split. rewrite <- K1; rewrite <- subst_eq_vars; intros x z_in_val. rewrite subst_rest_ok; trivial. destruct (var_in_subterm2 _ _ v_in_t) as [p Sub]. apply var_in_subterm with v_val p; trivial. apply (K2 (0 :: p)); trivial. split; trivial. intros p Sub; apply (K2 (0 :: p)); trivial. destruct (IHlt (tail_set _ Hlt)) with ls (subst_rest (var_list_list ls) sigma)as [Phi [K1 [K2 [K3 K4]]]]; trivial. intros; apply Wlt; right; trivial. intros; apply Wls; right; trivial. rewrite H0; apply map_eq. intros si si_in_ls; rewrite <- subst_eq_vars; intros x x_in_si; rewrite subst_rest_ok; trivial. destruct (in_split _ _ si_in_ls) as [ls1 [ls2 H]]; rewrite H; rewrite var_list_list_app; apply in_or_app; right; simpl; apply in_or_app; left; assumption. intros x u xu_in_rest_sig; apply (H1 x u); apply subst_rest_subst with (var_list_list ls); trivial. intros x u v xu_in_rest_sig xv_in_rest_sig; apply (H2 x u v); apply subst_rest_subst with (var_list_list ls); trivial. intros x y u xu_in_rest_sig yu_in_rest_sig; apply (H3 x y u); apply subst_rest_subst with (var_list_list ls); trivial. intro x; split. intro x_in_ls; assert (x_in_sig : In x (map (@fst _ _) sigma)). rewrite <- H4; simpl; apply in_or_app; right; assumption. rewrite in_map_iff in x_in_sig; destruct x_in_sig as [[x' u] [x_eq_x' x_in_sig]]; simpl in x_eq_x'; subst x'. rewrite in_map_iff; exists (x,u); split; trivial. apply subst_rest_subst_rest; trivial. intro x_in_rest_sig; rewrite in_map_iff in x_in_rest_sig; destruct x_in_rest_sig as [[x' u] [x_eq_x' x_in_rest_sig]]; simpl in x_eq_x'; subst x'. apply subst_rest_rest with sigma u; trivial. intros v v_in_lt; destruct (Aux2 v) as [v_val [K1 [K2 K3]]]. simpl; rewrite <- mem_or_app; right; assumption. exists v_val; split. rewrite <- K1; rewrite <- subst_eq_vars; intros x z_in_val. rewrite subst_rest_ok; trivial. destruct (mem_var_list_list _ _ v_in_lt) as [ti [ti_in_lt v_in_ti]]. destruct (var_in_subterm2 _ _ v_in_ti) as [p Sub]. destruct (in_split _ _ ti_in_lt) as [lt1 [lt2 Ht]]. rewrite Ht in H0; rewrite map_app in H0. destruct (split_map_set _ _ _ _ (sym_eq H0)) as [ls1 [ls2 [Hs [Hs1 Hs2]]]]. destruct ls2 as [ | si ls2]. discriminate. rewrite Hs; rewrite var_list_list_app; apply in_or_app; right; simpl; apply in_or_app; left. apply var_in_subterm with v_val p; trivial. subst lt ls. generalize (K2 ((1 + length lt1) :: p)); simpl. rewrite nth_error_at_pos. intro K2'; generalize (K2' Sub); clear K2'. replace (length lt1) with (length ls1). rewrite nth_error_at_pos; intro; assumption. rewrite <- (map_length (apply_subst sigma) ls1). rewrite Hs1; rewrite map_length; apply eq_refl. split; trivial. intros [ | i p]. intro; discriminate. generalize (K2 ((S i) :: p)); simpl; trivial. assert (u_in_s : forall x u, find X.eq_bool x phi = Some u -> forall x0 : T1.variable, In x0 (T1.var_list u) -> In x0 (var_list s)). intros x u x_phi. intros z z_in_u. assert (x_in_t : In x (var_list t)). rewrite <- k3; rewrite in_map_iff; exists (x,u); split; trivial. destruct (find_mem _ _ X.eq_bool_ok _ phi x_phi) as [x' [phi1 [phi2 [x_eq_x' H]]]]; subst x'. rewrite H; apply in_or_app; right; left; apply eq_refl. rewrite <- k2. destruct (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ x_in_t)) as [p Sub]. apply var_in_subterm with u p; trivial. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos t p phi). rewrite Sub; intro H; rewrite H; apply f_equal; simpl; rewrite x_phi; apply eq_refl. assert (v_in_ls : forall x v, find X.eq_bool x Phi = Some v -> forall x0 : T1.variable, In x0 (T1.var_list v) -> In x0 (var_list_list ls)). intros x v x_Phi. intros z z_in_v. assert (x_in_lt : In x (var_list_list lt)). rewrite <- K3; rewrite in_map_iff; exists (x,v); split; trivial. destruct (find_mem _ _ X.eq_bool_ok _ Phi x_Phi) as [x' [Phi1 [Phi2 [x_eq_x' H]]]]; subst x'. rewrite H; apply in_or_app; right; left; apply eq_refl. injection K2; clear K2; intro K2; rewrite <- K2. destruct (in_var_list_list _ _ x_in_lt) as [ti [ti_in_lt x_in_ti]]. destruct (in_split _ _ ti_in_lt) as [lt1 [lt2 H]]; rewrite H. simpl; rewrite map_app; rewrite var_list_list_app; apply in_or_app; right. simpl; apply in_or_app; left. destruct (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ x_in_ti)) as [p Sub]. apply var_in_subterm with (apply_subst Phi (Var x)) p. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos ti p Phi). rewrite Sub; intro H'; rewrite H'; apply f_equal; simpl; rewrite x_Phi; apply eq_refl. simpl; rewrite x_Phi; trivial. assert (ok : forall x u v, find X.eq_bool x phi = Some u -> find X.eq_bool x Phi = Some v -> u = v). intros x u v x_phi x_Phi. apply decompose_subst_aux with sigma; trivial. generalize (k4 x); rewrite x_phi; trivial. generalize (K4 x); rewrite x_Phi; trivial. intros z z_in_u; rewrite <- H4; simpl; apply in_or_app; left; apply u_in_s with x u; assumption. intros z z_in_v; rewrite <- H4; simpl; apply in_or_app; right; apply v_in_ls with x v; assumption. apply trans_eq with (apply_subst tau (Var x)). rewrite <- k1. rewrite subst_comp_is_subst_comp; simpl; rewrite x_phi. rewrite <- subst_eq_vars; intros z z_in_u; rewrite subst_rest_ok; trivial. apply u_in_s with x u; assumption. rewrite <- k3; rewrite in_map_iff; exists (x,u); split; trivial. destruct (find_mem _ _ X.eq_bool_ok _ phi x_phi) as [x' [phi1 [phi2 [x_eq_x' H]]]]; subst x'. rewrite H; apply in_or_app; right; left; apply eq_refl. rewrite <- K1. rewrite subst_comp_is_subst_comp; simpl; rewrite x_Phi. rewrite <- subst_eq_vars; intros z z_in_v; rewrite subst_rest_ok; trivial. apply v_in_ls with x v; assumption. rewrite <- K3; rewrite in_map_iff; exists (x,v); split; trivial. destruct (find_mem _ _ X.eq_bool_ok _ _ x_Phi) as [x' [Phi1 [Phi2 [x_eq_x' H]]]]; subst x'; rewrite H; apply in_or_app; right; left; apply eq_refl. exists (phi ++ Phi); split. simpl var_list_list; intros v v_in_tlt; destruct (in_app_or _ _ _ v_in_tlt) as [v_in_t | v_in_lt]; clear v_in_tlt. rewrite <- k1. do 2 rewrite subst_comp_is_subst_comp. simpl; rewrite find_app. generalize (mem_bool_ok _ _ X.eq_bool_ok v (map (fun st : T1.variable * T1.term => fst st) phi)). case (mem_bool X.eq_bool v (map (fun st : T1.variable * T1.term => fst st) phi)); [intro v_in_phi | intro v_not_in_phi]. case_eq (find X.eq_bool v phi); [intros v_val v_phi | intro v_phi]. rewrite <- subst_eq_vars; intros z z_in_v. rewrite subst_rest_ok; trivial. apply u_in_s with v v_val; trivial. assert (v_in_phi' : In v (map (fun st : T1.variable * T1.term => fst st) phi)). apply mem_impl_in with (@eq _); trivial. apply False_rect. rewrite in_map_iff in v_in_phi'; destruct v_in_phi' as [[v' v_val] [v_eq_v' v_in_phi']]; simpl in v_eq_v'; subst v'. apply (find_not_found X.eq_bool v v v_val phi v_phi (eq_var_bool_refl v) v_in_phi'). apply False_rect; apply v_not_in_phi; apply in_impl_mem. reflexivity. rewrite k3; assumption. assumption. rewrite <- K1. do 2 rewrite subst_comp_is_subst_comp. simpl; rewrite find_app. generalize (mem_bool_ok _ _ X.eq_bool_ok v (map (fun st : T1.variable * T1.term => fst st) phi)). case (mem_bool X.eq_bool v (map (fun st : T1.variable * T1.term => fst st) phi)); [intro v_in_phi | intro v_not_in_phi]. case_eq (find X.eq_bool v phi); [intros v_val v_phi | intro v_phi]. case_eq (find X.eq_bool v Phi); [intros v_Val v_Phi | intro v_Phi]. rewrite (ok _ _ _ v_phi v_Phi). rewrite <- subst_eq_vars; intros z z_in_v. rewrite subst_rest_ok; trivial. apply v_in_ls with v v_Val; trivial. apply False_rect. rewrite <- K3 in v_in_lt. rewrite in_map_iff in v_in_lt; destruct v_in_lt as [[v' v_Val] [v_eq_v' v_in_Phi]]; simpl in v_eq_v'; subst v'. apply (find_not_found X.eq_bool v v v_Val Phi v_Phi (eq_var_bool_refl v) v_in_Phi). assert (v_in_phi' : In v (map (fun st : T1.variable * T1.term => fst st) phi)). apply mem_impl_in with (@eq _); trivial. rewrite in_map_iff in v_in_phi'; destruct v_in_phi' as [[v' v_val] [v_eq_v' v_in_phi']]; simpl in v_eq_v'; subst v'. apply False_rect; apply (find_not_found X.eq_bool v v v_val phi v_phi (eq_var_bool_refl v) v_in_phi'). case_eq (find X.eq_bool v Phi); [intros v_Val v_Phi | intro v_Phi]. rewrite <- subst_eq_vars; intros z z_in_v. rewrite subst_rest_ok; trivial. apply v_in_ls with v v_Val; trivial. apply False_rect. rewrite <- K3 in v_in_lt. rewrite in_map_iff in v_in_lt; destruct v_in_lt as [[v' v_Val] [v_eq_v' v_in_Phi]]; simpl in v_eq_v'; subst v'. apply (find_not_found X.eq_bool v v v_Val Phi v_Phi (eq_var_bool_refl v) v_in_Phi). assumption. split. simpl; apply f_equal; apply f_equal2. rewrite <- k2; rewrite <- subst_eq_vars; intros v v_in_t. simpl; rewrite find_app. generalize (mem_bool_ok _ _ X.eq_bool_ok v (map (fun st : T1.variable * T1.term => fst st) phi)). case (mem_bool X.eq_bool v (map (fun st : T1.variable * T1.term => fst st) phi)); [intro v_in_phi | intro v_not_in_phi]. reflexivity. apply False_rect; apply v_not_in_phi; apply in_impl_mem; trivial. rewrite k3; assumption. injection K2; clear K2; intro K2. rewrite <- K2; apply map_eq. intros ti ti_in_lt; rewrite <- subst_eq_vars; intros v v_in_ti; simpl; rewrite find_app. generalize (mem_bool_ok _ _ X.eq_bool_ok v (map (fun st : T1.variable * T1.term => fst st) phi)). case (mem_bool X.eq_bool v (map (fun st : T1.variable * T1.term => fst st) phi)); [intro v_in_phi | intro v_not_in_phi]. case_eq (find X.eq_bool v phi); [intros v_val v_phi | intro v_phi]. case_eq (find X.eq_bool v Phi); [intros v_Val v_Phi | intro v_Phi]. apply (ok _ _ _ v_phi v_Phi). assert (v_in_lt : In v (var_list_list lt)). destruct (in_split _ _ ti_in_lt) as [lt1 [lt2 H]]; rewrite H; rewrite var_list_list_app; apply in_or_app; right; simpl; apply in_or_app; left; assumption. rewrite <- K3 in v_in_lt. rewrite in_map_iff in v_in_lt; destruct v_in_lt as [[v' v_Val] [v_eq_v' v_in_Phi]]; simpl in v_eq_v'; subst v'. apply False_rect; apply (find_not_found X.eq_bool v v v_Val Phi v_Phi (eq_var_bool_refl v) v_in_Phi). assert (v_in_phi' : In v (map (fun st : T1.variable * T1.term => fst st) phi)). apply mem_impl_in with (@eq _); trivial. rewrite in_map_iff in v_in_phi'; destruct v_in_phi' as [[v' v_val] [v_eq_v' v_in_phi']]; simpl in v_eq_v'; subst v'. apply False_rect; apply (find_not_found X.eq_bool v v v_val phi v_phi (eq_var_bool_refl v) v_in_phi'). reflexivity. split. intro v; rewrite map_app; simpl; split; intro H. simpl; destruct (in_app_or _ _ _ H) as [v_in_phi | v_in_Phi]. apply in_or_app; left; rewrite <- k3; assumption. apply in_or_app; right; rewrite <- K3; assumption. destruct (in_app_or _ _ _ H) as [v_in_phi | v_in_Phi]. apply in_or_app; left; rewrite k3; assumption. apply in_or_app; right; rewrite K3; assumption. intro v; simpl; rewrite find_app. case (mem_bool T1.eq_var_bool v (map (fun st : T1.variable * T1.term => fst st) phi)). apply (k4 v). apply (K4 v). Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)