diff options
Diffstat (limited to 'plugins/setoid_ring/Field_theory.v')
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 52b632a7d..bc947d54e 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1396,13 +1396,14 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) := Lemma fcons_ok : forall l l1, (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1. -intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1. 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. Section Fcons_simpl. |