# Library ac_matching.matching

``` 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. Module Type S. Declare Module Import Cf_eq_ac : cf_eq_ac.S. Import Cf_eq_ac.Ac. Import Sort. Import EqTh.T. Import F. Import LPermut. Record partly_solved_term : Set :=   mk_pst   {     head_symb : symbol;     new_var : variable;     closed_term : term   }. Record matching_problem : Set :=   mk_pb   {     existential_vars : list variable;     unsolved_part : list (term * term);     solved_part : substitution;     partly_solved_part : list (variable * partly_solved_term)   }. Definition is_rough_sol pb sigma :=  (forall t1 t2, In (t1,t2) pb.(unsolved_part) -> apply_cf_subst sigma t1 = t2) /\  (forall v, match find eq_variable_dec v pb.(partly_solved_part) with             | None => True             | Some pst =>               let l := (apply_cf_subst sigma (Var pst.(new_var))) :: pst.(closed_term) :: nil in               apply_cf_subst sigma (Var v) =              Term pst.(head_symb) (quicksort (flatten pst.(head_symb) l))              end) /\  (forall v, match find eq_variable_dec v pb.(solved_part) with             | None => True             | Some t => apply_cf_subst sigma (Var v) = t             end). Definition is_sol pb sigma :=   exists sigma', is_rough_sol pb sigma' /\                   (forall v, In v (existential_vars pb) \/                              apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v)). Fixpoint occurs_in_term (v : variable) (t : term) {struct t} : Prop :=   match t with   | Var v' => v=v'   | Term _ l =>       let occurs_in_term_list :=        (fix occurs_in_term_list v (l : list _) {struct l} : Prop :=         match l with         | nil => False         | h :: tl => (occurs_in_term v h) \/ (occurs_in_term_list v tl)         end) in         occurs_in_term_list v l     end. Fixpoint occurs_in_term_list (v : variable) (l : list term) {struct l} : Prop :=   match l with   | nil => False   | cons h tl => (occurs_in_term v h) \/ (occurs_in_term_list v tl)   end. Definition occurs_in_pb v pb :=  (occurs_in_term_list v (map (fun p => match p with | (t1,t2) => t1 end) pb.(unsolved_part))) \/  (match find eq_variable_dec v pb.(partly_solved_part) with    | None => False | Some _ => True end) \/  (match find eq_variable_dec v pb.(solved_part) with    | None => False | Some _ => True end). Parameter fresh_var : matching_problem -> variable. Parameter fresh_var_spec : forall pb, ~(occurs_in_pb (fresh_var pb) pb). Definition ac_elementary_solve_term_term_term pb f g lg list_of_terms l' list_of_equations : list matching_problem :=   map_without_repetition eq_term_dec   (fun t =>     match t with     | Term h _ =>       if eq_symbol_dec g h       then          match remove _ eq_term_dec t l' with            | None => None            | Some rmv =>               let t1' := build f list_of_terms in               let t2' := build f rmv in                 Some                   (mk_pb (existential_vars pb)                          (cons ((Term g lg),t) (cons (t1',t2') list_of_equations))                          (solved_part pb)                          (partly_solved_part pb))           end        else None     | Var _ => None     end)     l'. Definition ac_elementary_solve_term_var_with_val_term pb f x_val list_of_terms l' list_of_equations : list matching_problem :=   match remove _ eq_term_dec x_val l' with   | None =>      match x_val with      | Var _ => nil      | Term g ll =>          if eq_symbol_dec f g          then             match remove_list ll l' with             | Some rmv =>                if le_gt_dec (length list_of_terms) (length rmv)                then                    let t1' := build f list_of_terms in                    let t2' := build f rmv in                    let new_pb :=                    mk_pb (existential_vars pb)                    (cons (t1',t2') list_of_equations)                    (solved_part pb)                    (partly_solved_part pb) in                    cons new_pb nil                  else nil             | None => nil             end          else nil      end   | Some rmv =>     let t1' := build f list_of_terms in     let t2' := build f rmv in     let new_pb :=       mk_pb (existential_vars pb)       ((t1',t2') :: list_of_equations)             (solved_part pb)             (partly_solved_part pb) in       new_pb :: nil   end. Definition ac_elementary_solve_term_var_with_part_val_term pb f x_part_val list_of_terms l' list_of_equations : list matching_problem :=   if (eq_symbol_dec f (head_symb x_part_val))   then       match remove _ eq_term_dec (closed_term x_part_val) l' with       | None => nil       | Some rmv =>         let t1' := build f (cons (Var (new_var x_part_val)) list_of_terms) in         let t2' := build f rmv in         let new_pb :=           mk_pb (existential_vars pb)                 ((t1',t2') :: list_of_equations)                 (solved_part pb)                 (partly_solved_part pb) in          new_pb :: nil      end   else       map_without_repetition eq_term_dec        (fun t =>           match t with           | Term h l''' =>               if eq_symbol_dec h (head_symb x_part_val)               then                   match remove _ eq_term_dec (closed_term x_part_val) l''' with                   | None => None                   | Some rmv =>                     match remove _ eq_term_dec t l' with                     | None => None                     | Some rmv2 =>                       let y := new_var x_part_val in                       let y_val := build h rmv in                       let t1' := build f list_of_terms in                       let t2' := build f rmv2 in                       let new_pb :=                         mk_pb (existential_vars pb)                               ((Var y, y_val) :: (t1',t2') :: list_of_equations)                               (solved_part pb)                               (partly_solved_part pb) in                       Some new_pb                     end                   end               else None            | Var _ => None            end)          l'. Definition ac_elementary_solve_term_var_without_val_term pb f x list_of_terms l' list_of_equations : list matching_problem :=   map12_without_repetition eq_term_dec   (fun t =>     match remove _ eq_term_dec t l' with     | None => (None, None)     | Some rmv =>       let l'_without_t := rmv in       let t1' := build f list_of_terms in       let t2' := build f l'_without_t in       let new_pb :=         mk_pb (existential_vars pb)               ((t1', t2') :: list_of_equations)               ((x, t) :: (solved_part pb))               (partly_solved_part pb) in        if le_gt_dec (length l') ((length list_of_terms) + 1)        then (Some new_pb, None)        else          let y := fresh_var pb in          let t1'' := build f (Var y :: list_of_terms) in          let new_pb' :=            mk_pb (y :: existential_vars pb)                  ((t1'', t2') :: list_of_equations)                  (solved_part pb)                  ((x, mk_pst f y t) :: (partly_solved_part pb)) in           (Some new_pb, Some new_pb')     end)     l'. Definition ac_elementary_solve pb t1 t2 list_of_equations :=   match t1, t2 with   | (Term f (s :: list_of_terms as l)), (Term _ l') =>     match s with     | Term g lg =>         ac_elementary_solve_term_term_term           pb f g lg list_of_terms l' list_of_equations     | Var x =>       match find eq_variable_dec x (solved_part pb) with       | Some x_val =>          ac_elementary_solve_term_var_with_val_term            pb f x_val list_of_terms l' list_of_equations       | None =>         match find eq_variable_dec x (partly_solved_part pb) with         | Some x_part_val =>            ac_elementary_solve_term_var_with_part_val_term              pb f x_part_val list_of_terms l' list_of_equations         | None =>            ac_elementary_solve_term_var_without_val_term              pb f x list_of_terms l' list_of_equations         end       end     end   | (Term _ nil), (Term _ _) =>      let new_pb :=        mk_pb (existential_vars pb)              list_of_equations              (solved_part pb)              (partly_solved_part pb) in        new_pb :: nil   | _, _ => nil   end. Definition solve pb : list matching_problem :=   match unsolved_part pb with   | (tt1,tt2 as e) :: list_of_equations =>     match tt1, tt2 with     | Var x, _ =>       match find eq_variable_dec x (solved_part pb) with       | Some x_val =>         if eq_term_dec x_val tt2         then           let new_pb :=             mk_pb (existential_vars pb)             list_of_equations (solved_part pb) (partly_solved_part pb) in           new_pb :: nil         else nil       | None =>         match find eq_variable_dec x (partly_solved_part pb) with         | Some x_part_val =>           match tt2 with           | Var _ => nil           | Term f2 l2 =>             if eq_symbol_dec (head_symb x_part_val) f2             then               let y := new_var x_part_val in               match remove _ eq_term_dec (closed_term x_part_val) l2 with               | Some rmv =>                 let y_val := build f2 rmv in                 let new_pb :=                   mk_pb (existential_vars pb)                         ((Var y, y_val) :: list_of_equations)                         (solved_part pb) (partly_solved_part pb) in                   new_pb :: nil               | None => nil               end             else nil          end        | None =>            let new_pb :=              mk_pb (existential_vars pb)              list_of_equations ((x, tt2) :: (solved_part pb)) (partly_solved_part pb) in            new_pb :: nil        end      end     | Term f1 l1, Term f2 l2 =>         if eq_symbol_dec f1 f2         then             match arity f1 with             | Free _ =>               match fold_left2                 (fun current_list_of_eqs t1 t2 => (t1,t2) :: current_list_of_eqs)                 list_of_equations l1 l2 with               | Some new_list_of_equations =>                 let new_pb :=                   mk_pb (existential_vars pb)                   new_list_of_equations (solved_part pb) (partly_solved_part pb) in                 new_pb :: nil               | None => nil               end             | AC =>               if le_gt_dec (length l1) (length l2)               then ac_elementary_solve pb tt1 tt2 list_of_equations               else nil             | C =>               match l1, l2 with               | (s1 :: s2 :: nil), (t1 :: t2 :: nil) =>                 let new_pb1 :=                   mk_pb (existential_vars pb)                   ((s1,t1) :: (s2,t2) :: list_of_equations)                         (solved_part pb) (partly_solved_part pb) in                let new_pb2 :=                   mk_pb (existential_vars pb)                   ((s1,t2) :: (s2,t1) :: list_of_equations)                         (solved_part pb) (partly_solved_part pb) in                  new_pb1 :: new_pb2 :: nil                 | _, _ => nil               end             end         else nil     | _, _ => nil     end   | nil => nil end. Fixpoint well_sorted_partly_solved_part (l : list (variable * partly_solved_term)) : Prop :=  match l with  | nil => True  | (v,p) :: tl =>     v <> new_var p /\     (forall v', 1 <= nb_occ eq_variable_dec v' tl -> v' <> new_var p) /\     well_sorted_partly_solved_part tl end. Definition well_formed_pb pb := (forall t1 t2, In (t1,t2) pb.(unsolved_part) ->                    well_formed_cf t1 /\ well_formed_cf t2) /\ (forall v, match (find eq_variable_dec v pb.(solved_part)) with   | None => True   | Some t => well_formed_cf t   end) /\ (forall v, match (find eq_variable_dec v pb.(partly_solved_part)) with   | None => True   | Some pst =>       match arity pst.(head_symb) with       | AC => well_formed_cf pst.(closed_term) /\               match pst.(closed_term) with               | Var _ => True               | Term f _ => pst.(head_symb)<>f               end       | _ => False       end   end) /\ (forall v,   nb_occ eq_variable_dec v (solved_part pb) + nb_occ eq_variable_dec v (partly_solved_part pb) <= 1) /\ well_sorted_partly_solved_part (partly_solved_part pb) /\ (forall v p,   find eq_variable_dec v (partly_solved_part pb) = Some p -> occurs_in_pb (new_var p) pb). Definition is_well_formed_sol pb sigma :=  (exists sigma', is_rough_sol pb sigma' /\                   (forall v, In v (existential_vars pb) \/                       apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v)) /\                          (well_formed_cf_subst sigma')). Axiom list_permut_occurs_in_term_list :   forall v l1 l2, permut l1 l2 -> occurs_in_term_list v l1 ->   occurs_in_term_list v l2. Axiom add_new_var_to_rough_sol :   forall pb sigma t, well_formed_pb pb -> is_rough_sol pb sigma ->   (is_rough_sol pb ((fresh_var pb, t) :: sigma)). End S. Module Make (Cf_eq_ac1 : cf_eq_ac.S) : S with Module Cf_eq_ac := Cf_eq_ac1. Module Import Cf_eq_ac := Cf_eq_ac1. Import Ac. Import EqTh. Import T. Import F. Import X. Import Sort. Import LPermut. Record partly_solved_term : Set :=   mk_pst   {     head_symb : symbol;     new_var : variable;     closed_term : term   }. Record matching_problem : Set :=   mk_pb   {     existential_vars : list variable;     unsolved_part : list (term * term);     solved_part : substitution;     partly_solved_part : list (variable * partly_solved_term)   }. Definition is_rough_sol pb sigma :=  (forall t1 t2, In (t1,t2) pb.(unsolved_part) -> apply_cf_subst sigma t1 = t2) /\  (forall v, match find eq_variable_dec v pb.(partly_solved_part) with             | None => True             | Some pst =>               let l := (apply_cf_subst sigma (Var pst.(new_var))) :: pst.(closed_term) :: nil in               apply_cf_subst sigma (Var v) =              Term pst.(head_symb) (quicksort (flatten pst.(head_symb) l))              end) /\  (forall v, match find eq_variable_dec v pb.(solved_part) with             | None => True             | Some t => apply_cf_subst sigma (Var v) = t             end). Definition is_sol pb sigma :=   exists sigma', is_rough_sol pb sigma' /\                   (forall v, In v (existential_vars pb) \/                              apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v)). Fixpoint occurs_in_term (v : variable) (t : term) {struct t} : Prop :=   match t with   | Var v' => v=v'   | Term _ l =>       let occurs_in_term_list :=        (fix occurs_in_term_list v (l : list _) {struct l} : Prop :=         match l with         | nil => False         | h :: tl => (occurs_in_term v h) \/ (occurs_in_term_list v tl)         end) in         occurs_in_term_list v l     end. Fixpoint occurs_in_term_list (v : variable) (l : list term) {struct l} : Prop :=   match l with   | nil => False   | cons h tl => (occurs_in_term v h) \/ (occurs_in_term_list v tl)   end. Definition occurs_in_pb v pb :=  (occurs_in_term_list v (map (fun p => match p with | (t1,t2) => t1 end) pb.(unsolved_part))) \/  (match find eq_variable_dec v pb.(partly_solved_part) with    | None => False | Some _ => True end) \/  (match find eq_variable_dec v pb.(solved_part) with    | None => False | Some _ => True end). Parameter fresh_var : matching_problem -> variable. Parameter fresh_var_spec : forall pb, ~(occurs_in_pb (fresh_var pb) pb). Definition ac_elementary_solve_term_term_term pb f g lg list_of_terms l' list_of_equations : list matching_problem :=   map_without_repetition eq_term_dec   (fun t =>     match t with     | Term h _ =>       if eq_symbol_dec g h       then          match remove _ eq_term_dec t l' with            | None => None            | Some rmv =>               let t1' := build f list_of_terms in               let t2' := build f rmv in                 Some                   (mk_pb (existential_vars pb)                          (cons ((Term g lg),t) (cons (t1',t2') list_of_equations))                          (solved_part pb)                          (partly_solved_part pb))           end        else None     | Var _ => None     end)     l'. Definition ac_elementary_solve_term_var_with_val_term pb f x_val list_of_terms l' list_of_equations : list matching_problem :=   match remove _ eq_term_dec x_val l' with   | None =>      match x_val with      | Var _ => nil      | Term g ll =>          if eq_symbol_dec f g          then             match remove_list ll l' with             | Some rmv =>                if le_gt_dec (length list_of_terms) (length rmv)                then                    let t1' := build f list_of_terms in                    let t2' := build f rmv in                    let new_pb :=                    mk_pb (existential_vars pb)                    (cons (t1',t2') list_of_equations)                    (solved_part pb)                    (partly_solved_part pb) in                    cons new_pb nil                  else nil             | None => nil             end          else nil      end   | Some rmv =>     let t1' := build f list_of_terms in     let t2' := build f rmv in     let new_pb :=       mk_pb (existential_vars pb)       ((t1',t2') :: list_of_equations)             (solved_part pb)             (partly_solved_part pb) in       new_pb :: nil   end. Definition ac_elementary_solve_term_var_with_part_val_term pb f x_part_val list_of_terms l' list_of_equations : list matching_problem :=   if (eq_symbol_dec f (head_symb x_part_val))   then       match remove _ eq_term_dec (closed_term x_part_val) l' with       | None => nil       | Some rmv =>         let t1' := build f (cons (Var (new_var x_part_val)) list_of_terms) in         let t2' := build f rmv in         let new_pb :=           mk_pb (existential_vars pb)                 ((t1',t2') :: list_of_equations)                 (solved_part pb)                 (partly_solved_part pb) in          new_pb :: nil      end   else       map_without_repetition eq_term_dec        (fun t =>           match t with           | Term h l''' =>               if eq_symbol_dec h (head_symb x_part_val)               then                   match remove _ eq_term_dec (closed_term x_part_val) l''' with                   | None => None                   | Some rmv =>                     match remove _ eq_term_dec t l' with                     | None => None                     | Some rmv2 =>                       let y := new_var x_part_val in                       let y_val := build h rmv in                       let t1' := build f list_of_terms in                       let t2' := build f rmv2 in                       let new_pb :=                         mk_pb (existential_vars pb)                               ((Var y, y_val) :: (t1',t2') :: list_of_equations)                               (solved_part pb)                               (partly_solved_part pb) in                       Some new_pb                     end                   end               else None            | Var _ => None            end)          l'. Definition ac_elementary_solve_term_var_without_val_term pb f x list_of_terms l' list_of_equations : list matching_problem :=   map12_without_repetition eq_term_dec   (fun t =>     match remove _ eq_term_dec t l' with     | None => (None, None)     | Some rmv =>       let l'_without_t := rmv in       let t1' := build f list_of_terms in       let t2' := build f l'_without_t in       let new_pb :=         mk_pb (existential_vars pb)               ((t1', t2') :: list_of_equations)               ((x, t) :: (solved_part pb))               (partly_solved_part pb) in        if le_gt_dec (length l') ((length list_of_terms) + 1)        then (Some new_pb, None)        else          let y := fresh_var pb in          let t1'' := build f (Var y :: list_of_terms) in          let new_pb' :=            mk_pb (y :: existential_vars pb)                  ((t1'', t2') :: list_of_equations)                  (solved_part pb)                  ((x, mk_pst f y t) :: (partly_solved_part pb)) in           (Some new_pb, Some new_pb')     end)     l'. Definition ac_elementary_solve pb t1 t2 list_of_equations :=   match t1, t2 with   | (Term f (s :: list_of_terms as l)), (Term _ l') =>     match s with     | Term g lg =>         ac_elementary_solve_term_term_term           pb f g lg list_of_terms l' list_of_equations     | Var x =>       match find eq_variable_dec x (solved_part pb) with       | Some x_val =>          ac_elementary_solve_term_var_with_val_term            pb f x_val list_of_terms l' list_of_equations       | None =>         match find eq_variable_dec x (partly_solved_part pb) with         | Some x_part_val =>            ac_elementary_solve_term_var_with_part_val_term              pb f x_part_val list_of_terms l' list_of_equations         | None =>            ac_elementary_solve_term_var_without_val_term              pb f x list_of_terms l' list_of_equations         end       end     end   | (Term _ nil), (Term _ _) =>      let new_pb :=        mk_pb (existential_vars pb)              list_of_equations              (solved_part pb)              (partly_solved_part pb) in        new_pb :: nil   | _, _ => nil   end. Definition solve pb : list matching_problem :=   match unsolved_part pb with   | (tt1,tt2 as e) :: list_of_equations =>     match tt1, tt2 with     | Var x, _ =>       match find eq_variable_dec x (solved_part pb) with       | Some x_val =>         if eq_term_dec x_val tt2         then           let new_pb :=             mk_pb (existential_vars pb)             list_of_equations (solved_part pb) (partly_solved_part pb) in           new_pb :: nil         else nil       | None =>         match find eq_variable_dec x (partly_solved_part pb) with         | Some x_part_val =>           match tt2 with           | Var _ => nil           | Term f2 l2 =>             if eq_symbol_dec (head_symb x_part_val) f2             then               let y := new_var x_part_val in               match remove _ eq_term_dec (closed_term x_part_val) l2 with               | Some rmv =>                 let y_val := build f2 rmv in                 let new_pb :=                   mk_pb (existential_vars pb)                         ((Var y, y_val) :: list_of_equations)                         (solved_part pb) (partly_solved_part pb) in                   new_pb :: nil               | None => nil               end             else nil          end        | None =>            let new_pb :=              mk_pb (existential_vars pb)              list_of_equations ((x, tt2) :: (solved_part pb)) (partly_solved_part pb) in            new_pb :: nil        end      end     | Term f1 l1, Term f2 l2 =>         if eq_symbol_dec f1 f2         then             match arity f1 with             | Free _ =>               match fold_left2                 (fun current_list_of_eqs t1 t2 => (t1,t2) :: current_list_of_eqs)                 list_of_equations l1 l2 with               | Some new_list_of_equations =>                 let new_pb :=                   mk_pb (existential_vars pb)                   new_list_of_equations (solved_part pb) (partly_solved_part pb) in                 new_pb :: nil               | None => nil               end             | AC =>               if le_gt_dec (length l1) (length l2)               then ac_elementary_solve pb tt1 tt2 list_of_equations               else nil             | C =>               match l1, l2 with               | (s1 :: s2 :: nil), (t1 :: t2 :: nil) =>                 let new_pb1 :=                   mk_pb (existential_vars pb)                   ((s1,t1) :: (s2,t2) :: list_of_equations)                         (solved_part pb) (partly_solved_part pb) in                let new_pb2 :=                   mk_pb (existential_vars pb)                   ((s1,t2) :: (s2,t1) :: list_of_equations)                         (solved_part pb) (partly_solved_part pb) in                  new_pb1 :: new_pb2 :: nil                 | _, _ => nil               end             end         else nil     | _, _ => nil     end   | nil => nil end. Fixpoint well_sorted_partly_solved_part (l : list (variable * partly_solved_term)) : Prop :=  match l with  | nil => True  | (v,p) :: tl =>     v <> new_var p /\     (forall v', 1 <= nb_occ eq_variable_dec v' tl -> v' <> new_var p) /\     well_sorted_partly_solved_part tl end. Definition well_formed_pb pb := (forall t1 t2, In (t1,t2) pb.(unsolved_part) ->                    well_formed_cf t1 /\ well_formed_cf t2) /\ (forall v, match (find eq_variable_dec v pb.(solved_part)) with   | None => True   | Some t => well_formed_cf t   end) /\ (forall v, match (find eq_variable_dec v pb.(partly_solved_part)) with   | None => True   | Some pst =>       match arity pst.(head_symb) with       | AC => well_formed_cf pst.(closed_term) /\               match pst.(closed_term) with               | Var _ => True               | Term f _ => pst.(head_symb)<>f               end       | _ => False       end   end) /\ (forall v,   nb_occ eq_variable_dec v (solved_part pb) + nb_occ eq_variable_dec v (partly_solved_part pb) <= 1) /\ well_sorted_partly_solved_part (partly_solved_part pb) /\ (forall v p,   find eq_variable_dec v (partly_solved_part pb) = Some p -> occurs_in_pb (new_var p) pb). Lemma list_permut_occurs_in_term_list :   forall v l1 l2, permut l1 l2 -> occurs_in_term_list v l1 ->   occurs_in_term_list v l2. Proof. intros v; cut (forall l l', occurs_in_term_list v l' -> occurs_in_term_list v (l ++ l')). intros H l1; induction l1. contradiction. intros l2 P O. assert (a_in_l2 : In a l2). setoid_rewrite <- (list_permut.in_permut_in P); left; trivial. destruct (In_split _ _ a_in_l2) as [l2' [l2'' H']]; subst l2. elim O; clear O; intro O. apply H; left; trivial. setoid_rewrite <- permut_cons_inside in P. generalize (IHl1 (l2' ++ l2'') P O). clear l1 IHl1 P O; induction l2'. intro; right; trivial. simpl; intro O; destruct O as [ O | O ]. left; trivial. right; apply IHl2'; trivial; apply in_or_app; right; left; trivial. reflexivity. intro l; induction l; trivial; right; apply IHl; trivial. Qed. 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. intro t1; pattern t1; apply term_rec3; clear t1. intros v v0 t2 sigma O; simpl; elim (eq_variable_dec v v0). intro; subst v; cut False. contradiction. apply O; unfold occurs_in_term; trivial. intros; trivial. intros f l IH v t2 sigma O; simpl. cut (map (apply_cf_subst sigma) l = map (apply_cf_subst ((v,t2) :: sigma)) l). intro H; rewrite H; trivial. simpl in O; induction l. trivial. simpl; cut (apply_cf_subst sigma a = apply_cf_subst ((v,t2) :: sigma) a). intro H; rewrite H. cut (map (apply_cf_subst sigma) l = map (apply_cf_subst ((v,t2) :: sigma)) l). intro H1; rewrite H1; trivial. apply IHl. intros; apply IH; trivial; right; trivial. unfold not; intro O'; apply O; right; trivial. apply IH. left; trivial. unfold not; intro O'; apply O; left; trivial. Qed. Lemma add_new_var_to_rough_sol :   forall pb sigma t, well_formed_pb pb -> is_rough_sol pb sigma ->   (is_rough_sol pb ((fresh_var pb, t) :: sigma)). Proof. intros pb sigma t ; generalize (fresh_var_spec pb); unfold occurs_in_pb, is_rough_sol; intros O w S'; elim S'; clear S'; intros S1 S2; elim S2; clear S2; intros S2 S3; split. induction pb.(unsolved_part). contradiction. destruct a; intros t2 t3 I; elim I; clear I; intro I. inversion I. rewrite <- (add_new_var_to_subst t2 (fresh_var pb) t). apply S1; left; trivial. unfold not; intro O'; apply O. left; left; subst t2; trivial. apply IHl; trivial. unfold not; intro O'; apply O; elim O'; clear O'; intro O'. left; right; trivial. right; trivial. intros; apply S1; right; trivial. elim w; clear w; intros _ w; elim w; clear w; intros _ w; elim w; clear w; intros _ w; elim w; clear w; intros _ w; elim w; clear w; intros _ w; split. intro v; generalize (S2 v); cut (forall v', v=v' -> find eq_variable_dec v' (partly_solved_part pb) = find eq_variable_dec v (partly_solved_part pb)). case (find eq_variable_dec v (partly_solved_part pb)). intros p F; generalize (F v (refl_equal _)); clear F; intro F. repeat rewrite <- (add_new_var_to_subst); trivial. unfold not; intro O'; apply O. simpl in O'; rewrite O'. apply (w v p F). unfold not; intro O'; apply O. simpl in O'; rewrite O'. right; left; rewrite F; trivial. trivial. intros; subst v; trivial. intro v; generalize (S3 v); cut (forall v', v=v' -> find eq_variable_dec v' (solved_part pb) = find eq_variable_dec v (solved_part pb)). case (find eq_variable_dec v (solved_part pb)). intros t0 F; simpl; elim (eq_variable_dec v (fresh_var pb)). intro v_eq_fresh_var; absurd (v = fresh_var pb); trivial. unfold not; intros _; apply O; right; right; rewrite (F (fresh_var pb) v_eq_fresh_var); trivial. trivial. trivial. intros; subst v; trivial. Qed. Definition is_well_formed_sol pb sigma :=  (exists sigma', is_rough_sol pb sigma' /\                   (forall v, In v (existential_vars pb) \/                       apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v)) /\                          (well_formed_cf_subst sigma')). End Make. ```