proposition: Lemma ap_fm_tight : (tight_apart eq_fm ap_fm).
proof: Proof. unfold tight_apart. intros x. induction x. simpl. intro y. case y. red. unfold Not. intuition. intuition. intro y. simpl. case y. intuition. intros c l. generalize (IHx l). red. intro H0. elim H0. intros H1 H2. split. intro H3. split. red in H3. generalize (ap_tight A a c). intuition. apply H1. intro H4. apply H3. right. exact H4. intro H3. elim H3. clear H3. intros H3 H4. intro H5. elim H5. generalize (ap_tight A a c). intuition. apply H2. exact H4. Qed.
imports: CoRN.algebra.CSetoids