proposition: Lemma sameclass_spec `{WF} x y: reflect ({{t}} x y) (fst (equiv t x y)).
proof: Proof. intros. case_eq (fst (equiv t x y)); intro Heq; constructor. rewrite <- sameclass_equiv; trivial. intro F. rewrite <- sameclass_equiv in F. rewrite F in Heq. discriminate. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)