proposition: 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: 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. intro O'; apply O; destruct O' as [O' | O']; [ left | idtac ]; right; trivial. intros; apply S1; right; trivial. destruct w as [ _ [_ [_ [_ [_ w]]]]]; split. intro v; generalize (S2 v); case_eq (find X.eq_bool v (partly_solved_part pb)). intros p F; repeat rewrite <- (add_new_var_to_subst); trivial. intro O'; apply O; simpl in O'; rewrite O'; apply (w v p F). intro O'; apply O; simpl in O'; rewrite O'; right; left; rewrite F; trivial. trivial. intro v; generalize (S3 v); case_eq (find X.eq_bool v (solved_part pb)). intros t0 F; simpl; generalize (X.eq_bool_ok v (fresh_var pb)); case (X.eq_bool v (fresh_var pb)); [intro v_eq_fresh_var | intro v_diff_fresh_var]. apply False_rect; apply O. do 2 right; subst v; rewrite F; exact I. intro; assumption. intros _ _; exact I. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)