proposition: Lemma ap_irreflexive_unfolded : forall x : S, Not (x [#] x).
proof: Proof. Proof ap_irreflexive S. Lemma ap_cotransitive_unfolded : forall a b : S, a [#] b -> forall c : S, a [#] c or c [#] b. Proof. intros a b H c. exact (ap_cotransitive _ _ _ H c). Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid