proposition: Lemma op_involutive (C : Category) : (C^op)^op = C.
proof: Proof. unfold Opposite. unfold Opposite_obligation_1. unfold Opposite_obligation_2. unfold Opposite_obligation_3. simpl. destruct C. simpl. apply f_equal3; repeat (extensionality e; simpl; crush). extensionality b. extensionality c. extensionality d. extensionality f. extensionality g. extensionality h. crush. Qed.
imports: Hask.Prelude Hask.Crush Coq.Unicode.Utf8 FunctionalExtensionality