proposition: Lemma covee_hypothesis_opp : forall a u v, Category.axioms a -> covee_hypothesis (opp a) u v = vee_hypothesis a (flip u) (flip v).
proof: Proof. ir. ap iff_eq; ir. uh H0; uhg; ee. rwi mor_opp H0. am. wrr mor_opp. rw target_flip; try alike. rw target_flip; try alike. am. uh H0; ee. uhg; ee. rw mor_opp; am. rw mor_opp; am. rwi target_flip H2; try alike. rwi target_flip H2; try alike. am. wri mor_opp H1; alike. wri mor_opp H0; alike. Qed.
imports: Arith colimits little_cat fc_limits cardinal