diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-20 08:02:08 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-20 08:02:08 +0000 |
| commit | 0a59c2e537040d3e74fd65cd738fa617cbd4f1e2 (patch) | |
| tree | 125b5a5d46a346583372b46ab47b3b6a4292a11d /theories/Wellfounded | |
| parent | 2cf2a943e7140e50343bcb7d2eab24bebeeea9ec (diff) | |
Turning proofs of well-ordering of lexicographic product transparent
(see discussion on coq-club 5-6 Feb 2012).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15059 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Wellfounded')
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index ce0fee710..0e0961004 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -54,7 +54,7 @@ Section WfLexicographic_Product. subst x1. apply IHAcc0. elim inj_pair2 with A B x y' x0; assumption. - Qed. + Defined. Theorem wf_lexprod : well_founded leA -> @@ -65,7 +65,7 @@ Section WfLexicographic_Product. apply acc_A_B_lexprod; auto with sets; intros. red in wfB. auto with sets. - Qed. + Defined. End WfLexicographic_Product. @@ -88,7 +88,7 @@ Section Wf_Symmetric_Product. inversion_clear H5; auto with sets. apply IHAcc; auto. apply Acc_intro; trivial. - Qed. + Defined. Lemma wf_symprod : @@ -97,7 +97,7 @@ Section Wf_Symmetric_Product. red in |- *. destruct a. apply Acc_symprod; auto with sets. - Qed. + Defined. End Wf_Symmetric_Product. @@ -128,7 +128,7 @@ Section Swap. apply sp_noswap. apply left_sym; auto with sets. - Qed. + Defined. Lemma Acc_swapprod : @@ -156,7 +156,7 @@ Section Swap. apply right_sym; auto with sets. auto with sets. - Qed. + Defined. Lemma wf_swapprod : well_founded R -> well_founded SwapProd. @@ -164,6 +164,6 @@ Section Swap. red in |- *. destruct a; intros. apply Acc_swapprod; auto with sets. - Qed. + Defined. End Swap. |