intros.
generalize in match (ap_cotransitive_unfolded ? ? ? H1 a).
intro.elim H2.apply False_ind.apply (eq_imp_not_ap ? ? ? H).
intros.
generalize in match (ap_cotransitive_unfolded ? ? ? H1 a).
intro.elim H2.apply False_ind.apply (eq_imp_not_ap ? ? ? H).