diff options
Diffstat (limited to 'plugins/setoid_ring/Field_theory.v')
-rw-r--r-- | plugins/setoid_ring/Field_theory.v | 16 |
1 files changed, 9 insertions, 7 deletions
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. |