diff options
author | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
commit | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch) | |
tree | 7b000ad50dcc45ff1c63768a983cded1e23a07ca /plugins/setoid_ring/Field_theory.v | |
parent | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff) |
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
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. |