proposition: Lemma FEquiv_D : forall t t', FEquiv t t' -> (forall x, D t x O <-> D t' x O).
proof: Proof. intros . unfold FEquiv in H. rewrite 2 D_repr. apply H. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)