proposition: Lemma Fap_cotransitive : forall n : nat, cotransitive (Fap n).
proof: Proof. intro n. unfold cotransitive in |- *. unfold Fap in |- *. intros x y. case x. case y. intros x0 H0 x1 H1 H2 z. case z. intros x2 H. set (H5 := eq_nat_dec x2 x1) in *. elim H5. clear H5. intro H5. right. rewrite H5. exact H2. clear H5. intro H5. left. exact H5. Qed.
imports: CoRN.algebra.CSetoids