proposition: Lemma Fap_tight : forall n : nat, tight_apart (Feq n) (Fap n).
proof: Proof. unfold tight_apart in |- *. unfold Fap in |- *. unfold Feq in |- *. intros n x y. case x. case y. intros x0 H0 x1 H1. red in |- *. unfold not in |- *. unfold Not in |- *. intuition. Qed.
imports: CoRN.algebra.CSetoids