diff options
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/PermutSetoid.v | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index f1928a148..fa807c15f 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -342,8 +342,7 @@ Proof. rewrite if_eqA_refl in H. clear IHl; omega. rewrite IHl; intros. - specialize (H a0); auto with *. - destruct (eqA_dec a a0); simpl; auto with *. + specialize (H a0). omega. Qed. (** Permutation is compatible with InA. *) @@ -394,18 +393,14 @@ Proof. apply permut_length_1. red; red; intros. specialize (P a). simpl in *. - rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. - (** Bug omega: le "set" suivant ne devrait pas etre necessaire *) - set (u:= if eqA_dec a2 a then 1 else 0) in *; omega. + rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. omega. right. inversion_clear H0; [|inversion H]. split; auto. apply permut_length_1. red; red; intros. specialize (P a); simpl in *. - rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. - (** Bug omega: idem *) - set (u:= if eqA_dec b2 a then 1 else 0) in *; omega. + rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. omega. Qed. (** Permutation is compatible with length. *) |