proposition: Lemma covee_hypothesis_opp1 : forall a u v, Category.axioms a -> covee_hypothesis a u v -> vee_hypothesis (opp a) (flip u) (flip v).
proof: Proof. ir. uh H0; ee. uhg; ee. rww mor_opp. rww flip_flip. rww mor_opp. rww flip_flip. rw target_flip; try alike. rw target_flip; try alike. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal