2 files changed, 13 insertions, 9 deletions
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index 8ac952c0..013fd0ef 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -201,7 +201,8 @@ Ltac fold_field_cond req :=
 Ltac simpl_PCond FLD :=
   let req := get_FldEq FLD in
   let lemma := get_CondLemma FLD in
-  try apply lemma;
+  try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; 
+       clear lock_def lock);
   protect_fv "field_cond";
   fold_field_cond req;
   try exact I.
@@ -209,7 +210,8 @@ Ltac simpl_PCond FLD :=
 Ltac simpl_PCond_BEURK FLD :=
   let req := get_FldEq FLD in
   let lemma := get_CondLemma FLD in
-  apply lemma;
+  try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; 
+       clear lock_def lock);
   protect_fv "field_cond";
   fold_field_cond req.
 
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index bc05c252..1989e9b3 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1507,13 +1507,15 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
   | cons a l1 => Fcons a (Fapp l1 m)
   end.
 
-Lemma fcons_correct : forall l l1,
-  PCond l (Fapp l1 nil) -> PCond l l1.
-induction l1; simpl; intros.
- trivial.
- elim PCond_fcons_inv with (1 := H); intros.
-   destruct l1; auto.
-Qed.
+ Lemma fcons_correct : forall l l1,
+  (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1.
+ Proof.
+ intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1.
+ induction l1; simpl; intros.
+  trivial.
+  elim PCond_fcons_inv with (1 := H); intros.
+  destruct l1; trivial. split; trivial. apply IHl1; trivial.
+ Qed.
 
 End Fcons_impl.