# Library ac_matching.matching_well_formed

``` Add LoadPath "basis". Add LoadPath "term_algebra". Add LoadPath "term_orderings". Require Import Arith. Require Import List. Require Import more_list. Require Import list_sort. Require Import term. Require Import ac. Require Import cf_eq_ac. Require Import matching. Require Import matching_well_founded. Module Type S. Declare Module Import WFMatching : matching_well_founded.S. Import Matching. Import Cf_eq_ac. Import Ac. Import EqTh. Import T. Axiom well_formed_solve :  forall pb, well_formed_pb pb -> forall pb', In pb' (solve pb) -> well_formed_pb pb'. End S. Module Make (WFMatching1 : matching_well_founded.S) :   S with Module WFMatching := WFMatching1. Module Import WFMatching := WFMatching1. Import Matching. Import Cf_eq_ac. Import Ac. Import EqTh. Import T. Import F. Import X. Import Sort. Import LPermut. Theorem well_formed_solve :  forall pb, well_formed_pb pb -> forall pb', In pb' (solve pb) -> well_formed_pb pb'. Proof. unfold solve, well_formed_pb; intros pb [W1 [W2 [W3 [W4 [W5 W6]]]]] pb' In_pb'; assert (Fresh_var_spec :~ (occurs_in_term_list (fresh_var pb)     (map (fun p : term * term => let (t1, _) := p in t1) (unsolved_part pb)))). unfold not; intro; apply (fresh_var_spec pb); left; trivial. unfold occurs_in_pb in W6; destruct (unsolved_part pb) as [ | [[v1 | f1 l1] t2] l]. contradiction. assert (F : forall v, v=v1 -> find eq_variable_dec v (solved_part pb) = find eq_variable_dec v1 (solved_part pb)). intros; subst; trivial. destruct (find eq_variable_dec v1 (solved_part pb)) as [t1 | ]; generalize (F v1 (refl_equal _)); clear F; intro F. destruct (eq_term_dec t1 t2) as [t1_eq_t2 | _]; [idtac | contradiction]; inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]; subst. split; [intros; apply W1; right; trivial | idtac]. split; [intros; apply W2; right; trivial | idtac]. split; [intros; apply W3; right; trivial | idtac]. split; [intros; apply W4; right; trivial | idtac]. split; [intros; apply W5; right; trivial | idtac]. intros v p H; generalize (W6 v p H); intros [[H1 | H1'] | [H2 | H3]]. right; right; rewrite H1; simpl; rewrite F; trivial. left; trivial. right; left; trivial. right; right; trivial. generalize (W3 v1); assert (F' : forall v, v=v1 -> find eq_variable_dec v (partly_solved_part pb) = find eq_variable_dec v1 (partly_solved_part pb)). intros; subst; trivial. destruct (find eq_variable_dec v1 (partly_solved_part pb)) as [p1 | ]; generalize (F' v1 (refl_equal _)); clear F'; intro F'. destruct t2 as [ v2 | f2 l2]; [contradiction | idtac]; destruct (eq_symbol_dec (head_symb p1) f2) as [f1_eq_f2 | ]; [rewrite f1_eq_f2 | contradiction]; destruct_arity f2 n2 Af2; [ idtac | contradiction | contradiction]. intros [W_p1 H_p1]; generalize (in_remove _ eq_term_dec (closed_term p1) l2); destruct (remove _ eq_term_dec (closed_term p1) l2) as [ l2''' |]; [idtac | contradiction]. intros [cp1 [l2' [l2'' [ H [l2_eq l2'''_eq]]]]]. injection l2'''_eq; clear l2'''_eq; intro; subst l2'''; inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]; subst; split. intros t1 t2 [H | In_l]. inversion H; split; simpl; trivial. apply well_formed_cf_build_inside with (closed_term p1); trivial; refine (proj2 (A:= well_formed_cf (Var v1)) _); apply W1; left; trivial. apply W1; right; trivial. split; [intros; apply W2; right; trivial | idtac]. split; [intros; apply W3; right; trivial | idtac]. split; [intros; apply W4; right; trivial | idtac]. split; [intros; apply W5; right; trivial | idtac]. intros v p H; generalize (W6 v p H); intros [[H1 | H1'] | [H2 | H3]]. right; left; rewrite H1; simpl; rewrite F'; trivial. left; right; trivial. right; left; trivial. right; right; trivial. inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]. intros _; subst. split; [intros; apply W1; right; trivial | idtac]; split. intros v; simpl; destruct (eq_variable_dec v v1) as [_ | _]; [idtac | apply W2]; refine (proj2 (A:= well_formed_cf (Var v1)) _); apply W1; left; trivial. split; [intros; apply W3; right; trivial | idtac]; split. intros v; simpl; destruct (eq_variable_dec v v1) as [v_eq_v1 | _]; [idtac | apply W4]. subst v; rewrite (none_nb_occ_O _ _ _ F); rewrite (none_nb_occ_O _ _ _ F'); auto with arith. split; [intros; apply W5; right; trivial | idtac]. intros v p H; generalize (W6 v p H); intros [[H1 | H1'] | [H2 | H3]]. right; right; rewrite H1; simpl; destruct (eq_variable_dec v1 v1) as [ _ | v1_diff_v1]; trivial; absurd (v1 = v1); trivial. left; trivial. right; left; trivial. right; right; simpl; destruct (eq_variable_dec (new_var p) v1) as [ _ | _]; trivial. destruct t2 as [ v2 | f2 l2 ]; [contradiction | idtac]; destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | _]; [idtac | contradiction]. subst f2; destruct_arity f1 n1 Af1. destruct (le_gt_dec (length l1) (length l2)) as [_ | _]; [idtac | contradiction]. unfold ac_elementary_solve in *. assert (W_t1 : well_formed_cf (Term f1 l1)). refine (proj1 _ (B:= (well_formed_cf (Term f1 l2)))); apply W1; left; trivial. assert (W_t2 : well_formed_cf (Term f1 l2)). apply (proj2 (A:= (well_formed_cf (Term f1 l1)))); apply W1; left; trivial. destruct l1 as [ | t1 l1]. absurd (2 <= @length term nil); auto with arith; apply well_formed_cf_length with f1; trivial. destruct t1 as [v1 | g1 ll1]. generalize (W2 v1); assert (F : forall v, v=v1 -> find eq_variable_dec v (solved_part pb) = find eq_variable_dec v1 (solved_part pb)). intros; subst; trivial. destruct (find eq_variable_dec v1 (solved_part pb)) as [s1 | ]; generalize (F v1 (refl_equal _)); clear F; intro F. intro W_s1; unfold ac_elementary_solve_term_var_with_val_term in *. generalize (in_remove _ eq_term_dec s1 l2); destruct (remove _ eq_term_dec s1 l2) as [ l2''' |]. intros [cp1 [l2' [l2'' [ H [l2_eq l2'''_eq]]]]]. injection l2'''_eq; clear l2'''_eq; intro; subst l2'''; inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]; subst; split. intros t1 t2 [H | In_l]. inversion H; split. replace l1 with (nil ++ l1); trivial; apply well_formed_cf_build_inside with (Var v1); trivial. apply well_formed_cf_build_inside with cp1; trivial. apply W1; right; trivial. split; [intros; apply W2; right; trivial | idtac]. split; [intros; apply W3; right; trivial | idtac]. split; [intros; apply W4; right; trivial | idtac]. split; [intros; apply W5; right; trivial | idtac]. intros v p H; generalize (W6 v p H); intros [[[H1 | H1'] | H1''] | [H2 | H3]]. right; right; rewrite H1; simpl; rewrite F; trivial. left; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac]; simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1); trivial; apply quick_permut. left; right; trivial. right; left; trivial. right; right; trivial. intros _; destruct s1 as [| g1 ll1]; [contradiction | idtac ]; destruct (eq_symbol_dec f1 g1) as [f1_eq_g1 | _]; [idtac | contradiction]. assert (S_ll1 : is_sorted ll1). apply well_formed_cf_sorted with g1; subst; trivial. assert (S_l2 : is_sorted l2). apply well_formed_cf_sorted with f1; trivial. generalize (in_remove_list S_ll1 S_l2); unfold EDS.A, DOS.A in *; destruct (remove_list ll1 l2) as [l2' | ]; [idtac | contradiction ]. unfold EDS.A, DOS.A in *; destruct (le_gt_dec (length l1) (length l2')) as [L_l1_l2' |]; [idtac | contradiction]. inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]; intro P; subst; split. intros t1 t2 [H | In_l]. inversion H; split. replace l1 with (nil ++ l1); trivial; apply well_formed_cf_build_inside with (Var v1); trivial. assert (In_l2'_In_l2 : forall t, In t l2' -> In t l2). intros t In_l2'; setoid_rewrite <- (list_permut.in_permut_in P); apply in_or_app; right; trivial. apply well_formed_cf_build; trivial. apply le_trans with (length l1); trivial; apply le_S_n; replace (S (length l1)) with (length (Var v1 :: l1)); trivial; apply well_formed_cf_length with g1; trivial. intros t In_l2'; apply well_formed_cf_subterms with g1 l2; trivial; apply In_l2'_In_l2; trivial. intros t In_l2'; apply well_formed_cf_alien with l2; trivial; apply In_l2'_In_l2; trivial. apply W1; right; trivial. split; [intros; apply W2; right; trivial | idtac]. split; [intros; apply W3; right; trivial | idtac]. split; [intros; apply W4; right; trivial | idtac]. split; [intros; apply W5; right; trivial | idtac]. intros v p H; generalize (W6 v p H); intros [[[H1 | H1'] | H1''] | [H2 | H3]]. right; right; rewrite H1; simpl; rewrite F; trivial. left; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac]; simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1); trivial; apply quick_permut. left; right; trivial. right; left; trivial. right; right; trivial. intros _; generalize (W3 v1); assert (F' : forall v, v=v1 -> find eq_variable_dec v (partly_solved_part pb) = find eq_variable_dec v1 (partly_solved_part pb)). intros; subst; trivial. destruct (find eq_variable_dec v1 (partly_solved_part pb)) as [p1 | ]; generalize (F' v1 (refl_equal _)); clear F'; intro F'. unfold ac_elementary_solve_term_var_with_part_val_term in *. destruct (eq_symbol_dec f1 (head_symb p1)) as [f1_eq_hd_p1 | f1_diff_hd_p1]. generalize (in_remove _ eq_term_dec (closed_term p1) l2); destruct (remove _ eq_term_dec (closed_term p1) l2) as [l2''' | ]; [idtac | contradiction]. inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]. intros [cp1 [l2' [l2'' [ H [l2_eq l2'''_eq]]]]]. injection l2'''_eq; clear l2'''_eq; intro; subst; split. intros t1 t2 [H'' | In_l]. replace t1 with (fst (t1,t2)); trivial; rewrite <- H''; replace t2 with (snd (t1,t2)); trivial; rewrite <- H''; unfold fst, snd; split. apply well_formed_cf_build; trivial. simpl; auto with arith. intros t [t_eq | In_t_l1]; [subst; simpl; trivial | idtac]; apply well_formed_cf_subterms with (head_symb p1) (Var v1 :: l1); trivial; right; trivial. intros t [t_eq | In_t_l1]; [subst; simpl; trivial | idtac]. apply well_formed_cf_alien with (Var v1 :: l1); trivial; right; trivial. apply well_formed_cf_build_inside with (closed_term p1); trivial. apply W1; right; trivial. split; [intros; apply W2; right; trivial | idtac]. split; [intros; apply W3; right; trivial | idtac]. split; [intros; apply W4; right; trivial | idtac]. split; [intros; apply W5; right; trivial | idtac]. intros v p H''; generalize (W6 v p H''); intros [[[H1 | H1'] | H1''] | [H2 | H3]]. right; left; rewrite H1; simpl; rewrite F'; trivial. left; left; destruct l1 as [ | u1 l1]; [contradiction | idtac]. simpl; apply list_permut_occurs_in_term_list with (Var (new_var p1) :: u1 :: l1); [ apply quick_permut | idtac]; right; trivial. left; right; trivial. right; left; trivial. right; right; trivial. intros W3_v1; pattern pb'; refine (prop_map_without_repetition (B:=matching_problem) eq_term_dec _ _ _ _ pb' In_pb'); clear pb' In_pb'; intros [ | g2 ll2] In_t2; trivial; destruct (eq_symbol_dec g2 (head_symb p1)) as [g2_eq_hd_p1 | g2_diff_hd_p1]; trivial. generalize (in_remove _ eq_term_dec (closed_term p1) ll2); destruct (remove _ eq_term_dec (closed_term p1) ll2) as [ll2''' | ]; trivial. intros [cp1 [ll2' [ll2'' [ H [ll2_eq ll2'''_eq]]]]]. injection ll2'''_eq; clear ll2'''_eq; intro; subst ll2'''; generalize (in_remove _ eq_term_dec (Term g2 ll2) l2); destruct (remove _ eq_term_dec (Term g2 ll2) l2) as [l2''' | ]; trivial. intros [cp1' [l2' [l2'' [ H' [l2_eq l2'''_eq]]]]]. injection l2'''_eq; clear l2'''_eq; intro; subst; split. intros t1 t2 [H'' | [H'' | In_l]]. inversion H''; split; simpl; trivial; subst. apply well_formed_cf_build_inside with (closed_term p1). destruct (arity (head_symb p1)) as [ | | n]; [trivial | contradiction | contradiction]. apply (well_formed_cf_subterms W_t2); apply in_or_app; right; left; trivial. inversion H''; split; subst. replace l1 with (nil ++ l1); trivial; replace (Var v1 :: l1) with (nil ++ Var v1 :: l1) in W_t1; trivial; apply well_formed_cf_build_inside with (Var v1); trivial. apply well_formed_cf_build_inside with (Term (head_symb p1) (ll2' ++ closed_term p1 :: ll2'')); trivial. apply W1; right; trivial. split; [intros; apply W2; right; trivial | idtac]. split; [intros; apply W3; right; trivial | idtac]. split; [intros; apply W4; right; trivial | idtac]. split; [intros; apply W5; right; trivial | idtac]. intros v p H''; generalize (W6 v p H''); intros [[[H1 | H1'] | H1''] | [H2 | H3]]. right; left; rewrite H1; simpl; rewrite F'; trivial. left; right; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac]. simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1); [ apply quick_permut | idtac]; trivial. left; right; right; trivial. right; left; trivial. right; right; trivial. intros _; unfold ac_elementary_solve_term_var_without_val_term in *. pattern pb'; refine (prop_map12_without_repetition (B:=matching_problem) eq_term_dec _ _ _ _ pb' In_pb'); clear pb' In_pb'; intros t2 In_t2; generalize (in_remove _ eq_term_dec t2 l2); destruct (remove _ eq_term_dec t2 l2) as [l2''' | ]; trivial. intros [cp1' [l2' [l2'' [ H' [l2_eq l2'''_eq]]]]]. injection l2'''_eq; clear l2'''_eq; intro; subst l2'''; unfold DOS.A, EDS.A in *; destruct (le_gt_dec (length l2) (length l1 + 1)) as [_ | _]; trivial. split. intros t1 t3 [H'' | In_l]. inversion H''; split; simpl; trivial; subst. replace l1 with (nil ++ l1); trivial; replace (Var v1 :: l1) with (nil ++ Var v1 :: l1) in W_t1; trivial; apply well_formed_cf_build_inside with (Var v1); trivial. apply well_formed_cf_build_inside with cp1'; trivial. apply W1; right; trivial. split. intro v; simpl; destruct (eq_variable_dec v v1) as [_ | _]; [ apply well_formed_cf_subterms with f1 l2; trivial | apply W2 ]. split; [intros; apply W3; right; trivial | idtac]. split. intro v; simpl; destruct (eq_variable_dec v v1) as [v_eq_v1 | _]. subst; rewrite (none_nb_occ_O _ _ _ F); rewrite (none_nb_occ_O _ _ _ F'); auto with arith. apply W4. split; [intros; apply W5; right; trivial | idtac]. intros v p H''; generalize (W6 v p H''); intros [[[H1 | H1'] | H1''] | [H2 | H3]]. right; right; rewrite H1; simpl; destruct (eq_variable_dec v1 v1) as [_ | v1_diff_v1]; [idtac | absurd (v1 = v1)]; trivial. left; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac]; simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1); trivial; apply quick_permut. left; right; trivial. right; left; trivial. right; right; simpl; destruct (eq_variable_dec (new_var p) v1) as [_ | _]; trivial. split. split. intros t1 t3 [H'' | In_l]. inversion H''; split; simpl; trivial; subst. replace l1 with (nil ++ l1); trivial; replace (Var v1 :: l1) with (nil ++ Var v1 :: l1) in W_t1; trivial; apply well_formed_cf_build_inside with (Var v1); trivial. apply well_formed_cf_build_inside with cp1'; trivial. apply W1; right; trivial. split. intro v; simpl; destruct (eq_variable_dec v v1) as [_ | _]; [ apply well_formed_cf_subterms with f1 l2; trivial | apply W2 ]. split; [intros; apply W3; right; trivial | idtac]. split. intro v; simpl; destruct (eq_variable_dec v v1) as [v_eq_v1 | _]. subst; rewrite (none_nb_occ_O _ _ _ F); rewrite (none_nb_occ_O _ _ _ F'); auto with arith. apply W4. split; [intros; apply W5; right; trivial | idtac]. intros v p H''; generalize (W6 v p H''); intros [[[H1 | H1'] | H1''] | [H2 | H3]]. right; right; rewrite H1; simpl; destruct (eq_variable_dec v1 v1) as [_ | v1_diff_v1]; [idtac | absurd (v1 = v1)]; trivial. left; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac]; simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1); trivial; apply quick_permut. left; right; trivial. right; left; trivial. right; right; simpl; destruct (eq_variable_dec (new_var p) v1) as [_ | _]; trivial. split. intros t1 t3 [H'' | In_l]. replace t1 with (fst (t1,t3)); trivial; rewrite <- H''; unfold fst; replace t3 with (snd (t1,t3)); trivial; rewrite <- H''; unfold snd; split. apply well_formed_cf_build; trivial. simpl; auto with arith. intros t [t_eq | In_t_l1]; [subst t; simpl; trivial | idtac]; apply well_formed_cf_subterms with f1 (Var v1 :: l1); trivial; right; trivial. intros t [t_eq | In_t_l1]; [subst t; simpl; trivial | idtac]; apply well_formed_cf_alien with (Var v1 :: l1); trivial; right; trivial. subst; apply well_formed_cf_build_inside with cp1'; trivial. apply W1; right; trivial. split; [intros; apply W2; right; trivial | idtac]. split. intro v; simpl; destruct (eq_variable_dec v v1) as [_ | _]. simpl; rewrite Af1; split. apply well_formed_cf_subterms with f1 l2; trivial. apply well_formed_cf_alien with l2; trivial. apply W3. split. intro v; simpl; destruct (eq_variable_dec v v1) as [v_eq_v1 | _]. subst; rewrite (none_nb_occ_O _ _ _ F); rewrite (none_nb_occ_O _ _ _ F'); auto with arith. apply W4. split. unfold well_sorted_partly_solved_part; split; [idtac | split; [idtac | apply W5]]. simpl; intro; apply Fresh_var_spec; left; left; subst v1; simpl; trivial. unfold new_var; intros v' one_v' v'_eq_fresh_var_pb; apply (fresh_var_spec pb); right; left; rewrite <- v'_eq_fresh_var_pb. generalize (none_nb_occ_O eq_variable_dec v' (partly_solved_part pb)); destruct (find eq_variable_dec v' (partly_solved_part pb)); trivial; intro H; generalize (H (refl_equal _)); clear H; intro H; rewrite H in one_v'; absurd (1 <= 0); trivial; auto with arith. simpl; intros v p H; destruct (eq_variable_dec v v1) as [_ | v_diff_v1]. injection H; clear H; intro H; subst p; simpl. left; left; destruct l1 as [ | u1 l1]; simpl; [trivial | idtac]; apply list_permut_occurs_in_term_list with (Var (fresh_var pb) :: u1 :: l1); [apply quick_permut | left; simpl; trivial]. generalize (W6 _ _ H); intros [[[H1 | H1'] | H1''] | [H2 | H3]]. right; left; simpl; destruct (eq_variable_dec (new_var p) v1) as [_ | new_var_p_diff_v1]; trivial; absurd (new_var p = v1); trivial. left; left; destruct l1 as [ | u1 l1]; simpl; [contradiction | idtac]; apply list_permut_occurs_in_term_list with (Var (fresh_var pb) :: u1 :: l1); [apply quick_permut | right; trivial]. left; right; trivial. right; left; simpl; destruct (eq_variable_dec (new_var p) v1) as [_ | _]; trivial. right; right; trivial. unfold ac_elementary_solve_term_term_term in *. pattern pb'; refine (prop_map_without_repetition (B:=matching_problem) eq_term_dec _ _ _ _ pb' In_pb'); clear pb' In_pb'; intros [ | g2 ll2] In_t2; trivial; destruct (eq_symbol_dec g1 g2) as [g1_eq_g2 | g1_diff_g2]; trivial. generalize (in_remove _ eq_term_dec (Term g2 ll2) l2); destruct (remove _ eq_term_dec (Term g2 ll2) l2) as [l2''' | ]; trivial. intros [cp1' [l2' [l2'' [ H' [l2_eq l2'''_eq]]]]]. injection l2'''_eq; clear l2'''_eq; intro; subst l2'''; split. intros t1 t2 [H | [H | In_l]]; [idtac | idtac | apply W1; right; trivial]. injection H; clear H; intros; subst t1 t2; split. apply (well_formed_cf_subterms W_t1); left; trivial. apply (well_formed_cf_subterms W_t2); subst l2 cp1'; apply in_or_app; right; left; trivial. injection H; clear H; intros; subst t1 t2; split. replace l1 with (nil ++ l1); trivial; replace (Term g1 ll1 :: l1) with (nil ++ Term g1 ll1 :: l1) in W_t1; trivial; apply well_formed_cf_build_inside with (Term g1 ll1); trivial. subst; apply well_formed_cf_build_inside with (Term g2 ll2); trivial. split; [intros; apply W2; right; trivial | idtac]. split; [intros; apply W3; right; trivial | idtac]. split; [intros; apply W4; right; trivial | idtac]. split; [intros; apply W5; right; trivial | idtac]. intros v p H; generalize (W6 v p H); intros [[[H1 | H1'] | H1''] | [H2 | H3]]. left; left; trivial. left; right; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac]; simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1); trivial; apply quick_permut. left; right; right; trivial. right; left; trivial. right; right; trivial. destruct l1 as [ | u1 [ | u2 [ | u3 l1]]]; [contradiction | contradiction | idtac | contradiction]. destruct l2 as [ | v1 [ | v2 [ | v3 l2]]]; [contradiction | contradiction | idtac | contradiction]. inversion_clear In_pb' as [pb'_eq_ | In_pb'']; [idtac | inversion_clear In_pb'' as [pb''_eq_ | ]; [idtac | contradiction]]; subst. split. intros t1 t2 [H | [H | In_l]]; [idtac | idtac | apply W1; right; trivial]. injection H; clear H; intros; subst t1 t2; split. apply well_formed_cf_subterms with f1 (u1 :: u2 :: nil); [idtac | left; trivial]; refine (proj1 _ (B:= (well_formed_cf (Term f1 (v1 :: v2 :: nil))))); apply W1; left; trivial. apply well_formed_cf_subterms with f1 (v1 :: v2 :: nil); [idtac | left; trivial]; apply (proj2 (A:= (well_formed_cf (Term f1 (u1 :: u2 :: nil))))); apply W1; left; trivial. injection H; clear H; intros; subst t1 t2; split. apply well_formed_cf_subterms with f1 (u1 :: u2 :: nil); [idtac | right; left; trivial]; refine (proj1 _ (B:= (well_formed_cf (Term f1 (v1 :: v2 :: nil))))); apply W1; left; trivial. apply well_formed_cf_subterms with f1 (v1 :: v2 :: nil); [idtac | right; left; trivial]; apply (proj2 (A:= (well_formed_cf (Term f1 (u1 :: u2 :: nil))))); apply W1; left; trivial. split; [intros; apply W2; right; trivial | idtac]. split; [intros; apply W3; right; trivial | idtac]. split; [intros; apply W4; right; trivial | idtac]. split; [intros; apply W5; right; trivial | idtac]. intros v p H; generalize (W6 v p H); intros [[[H1 | [H1' | H1'']] | H1'''] | [H2 | H3]]. left; left; trivial. left; right; left; trivial. contradiction. left; right; right; trivial. right; left; trivial. right; right; trivial. split. intros t1 t2 [H | [H | In_l]]; [idtac | idtac | apply W1; right; trivial]. injection H; clear H; intros; subst t1 t2; split. apply well_formed_cf_subterms with f1 (u1 :: u2 :: nil); [idtac | left; trivial]; refine (proj1 _ (B:= (well_formed_cf (Term f1 (v1 :: v2 :: nil))))); apply W1; left; trivial. apply well_formed_cf_subterms with f1 (v1 :: v2 :: nil); [idtac | right; left; trivial]; apply (proj2 (A:= (well_formed_cf (Term f1 (u1 :: u2 :: nil))))); apply W1; left; trivial. injection H; clear H; intros; subst t1 t2; split. apply well_formed_cf_subterms with f1 (u1 :: u2 :: nil); [idtac | right; left; trivial]; refine (proj1 _ (B:= (well_formed_cf (Term f1 (v1 :: v2 :: nil))))); apply W1; left; trivial. apply well_formed_cf_subterms with f1 (v1 :: v2 :: nil); [idtac | left; trivial]; apply (proj2 (A:= (well_formed_cf (Term f1 (u1 :: u2 :: nil))))); apply W1; left; trivial. split; [intros; apply W2; right; trivial | idtac]. split; [intros; apply W3; right; trivial | idtac]. split; [intros; apply W4; right; trivial | idtac]. split; [intros; apply W5; right; trivial | idtac]. intros v p H; generalize (W6 v p H); intros [[[H1 | [H1' | H1'']] | H1'''] | [H2 | H3]]. left; left; trivial. left; right; left; trivial. contradiction. left; right; right; trivial. right; left; trivial. right; right; trivial. assert (L12 : length l1 = length l2). apply trans_eq with n1; [idtac | apply sym_eq]; generalize (W1 (Term f1 l1) (Term f1 l2) (or_introl _ (refl_equal _))); intros [[_ W_t1] [_ W_t2]]; [rewrite Af1 in W_t1 | rewrite Af1 in W_t2]; trivial. split. assert (W1_l : forall t1 t2, In (t1,t2) l -> well_formed_cf t1 /\ well_formed_cf t2). intros; apply W1; right; trivial. assert (W_l1 : forall t, In t l1 -> well_formed_cf t). intros; apply well_formed_cf_subterms with f1 l1; trivial; refine (proj1 _ (B:= (well_formed_cf (Term f1 l2)))); apply W1; left; trivial. assert (W_l2 : forall t, In t l2 -> well_formed_cf t). intros; apply well_formed_cf_subterms with f1 l2; trivial; apply (proj2 (A:= (well_formed_cf (Term f1 l1)))); apply W1; left; trivial. generalize l l2 In_pb' L12 W1_l W_l1 W_l2; simpl; clear W1 W2 W3 W4 W5 W6 Fresh_var_spec l l2 In_pb' L12 W1_l W_l1 W_l2; induction l1 as [ | t1 l1]; destruct l2 as [ | t2 l2]. intros [In_pb' | In_pb'] _; [idtac | contradiction]; subst pb'; simpl; trivial. intros _ L12; simpl L12; discriminate. intros _ L12; simpl L12; discriminate. intros In_pb' L12; simpl in L12; generalize (eq_add_S _ _ L12); clear L12; intro L12; intros W1_l W_l1 W_l2; intros; apply IHl1 with ((t1, t2) :: l) l2; trivial. intros t4 t5 [H' | In_l]. injection H'; split; subst; [apply W_l1 | apply W_l2]; left; trivial. apply W1_l; trivial. intros; apply W_l1; right; trivial. intros; apply W_l2; right; trivial. assert (H : forall l', l' = l -> fold_left2 (fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>                 (t1, t2) :: current_list_of_eqs) l' l1 l2 = fold_left2 (fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>                 (t1, t2) :: current_list_of_eqs) l l1 l2). intros; subst; trivial. destruct (fold_left2                (fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>                 (t1, t2) :: current_list_of_eqs) l l1 l2) as [new_list_of_equations | ]; generalize (H l (refl_equal _)); clear H; intro H; [idtac | contradiction]. destruct In_pb' as [pb'_eq | ]; [idtac | contradiction]; subst. split; [intros; apply W2; right; trivial | idtac]. split; [intros; apply W3; right; trivial | idtac]. split; [intros; apply W4; right; trivial | idtac]. split; [intros; apply W5; right; trivial | idtac]. assert (H' : forall l1 l new_list_of_equations l2, fold_left2 (fun cl (t1 t2 : term) => (t1, t2) :: cl) l l1 l2 = Some new_list_of_equations ->    forall u1 u2, In (u1, u2) l -> In (u1, u2) new_list_of_equations). clear l l1 l2 W1 W6 Fresh_var_spec L12 H new_list_of_equations. induction l1 as [ | v1 l1]. intros l new_list_of_equations [ | v2 l2]; simpl; [idtac | intros; discriminate]; intros H; injection H; intro; subst; trivial. intros l new_list_of_equations [| v2 l2]; simpl; [intros; discriminate | idtac]. intros; apply IHl1 with ((v1,v2) :: l) l2; trivial; right; trivial. intros v p H''; generalize (W6 v p H''); intros [ [H1 | H1'] | [H2 | H3]]. left; simpl occurs_in_term in H1; unfold unsolved_part. generalize l l2 L12 H H1; clear l l2 W1 W6 Fresh_var_spec L12 H H1; induction l1 as [ | u1 l1]; [contradiction | idtac]. intros l [| u2 l2] L12 H; [discriminate | idtac]; intros [In_u1 | In_l1]. assert (In_u1_new_list : In (u1,u2) new_list_of_equations). simpl in H; apply H' with l1 ((u1,u2) :: l) l2; trivial; left; trivial. generalize new_list_of_equations In_u1_new_list; clear new_list_of_equations H'' IHl1 H In_u1_new_list; induction new_list_of_equations as [| [w1 w2] nle]; [contradiction | idtac]. intros [u12_eq | In_u12]; [injection u12_eq; intros; subst; left; trivial | idtac]. right; apply IHnle; trivial. apply IHl1 with ((u1,u2) :: l) l2; trivial; apply eq_add_S; trivial. left; assert (H''' : exists u1, exists u2, occurs_in_term (new_var p) u1 /\ In (u1, u2) l). generalize (new_var p) l H1'; clear l H1' W1 W6 Fresh_var_spec H H''; induction l as [ | [u1 u2] l]; [contradiction | idtac]; intros [u12_eq | In_u12]. exists u1; exists u2; intuition. generalize (IHl In_u12); intros [u3 [u4 [H1 H2]]]; exists u3; exists u4; split; trivial; right; trivial. generalize H'''; clear H'''; intros [u1 [u2 [H''' In_u12]]]; generalize (H' _ _ _ _ H _ _ In_u12); clear l W1 W6 Fresh_var_spec H H1' In_u12 H''; induction new_list_of_equations as [ | [v1 v2] nle]; [contradiction | idtac]; intros [u12_eq | In_u12]. injection u12_eq; intros; subst; left; trivial. right; apply IHnle; trivial. right; left; trivial. right; right; trivial. Qed. End Make. ```