1 files changed, 2 insertions, 11 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index b58998d1fe..d286b190f7 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -93,21 +93,12 @@ Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A)
    : Irreflexive (complement R).
 
   Next Obligation. 
-  Proof. 
-    unfold complement.
-    red. intros H.
-    intros H' ; apply H'.
-    apply reflexivity.
-  Qed.
-
+  Proof. firstorder. Qed.
 
 Program Instance complement_Symmetric [ Symmetric A (R : relation A) ] : Symmetric (complement R).
 
   Next Obligation.
-  Proof.
-    red ; intros H'.
-    apply (H (symmetry H')).
-  Qed.
+  Proof. firstorder. Qed.
 
 (** * Standard instances. *)