proposition: Lemma equiv_reflexive_false : forall `{WF} x, ~ fst (equiv t x x) = false .
proof: Proof. intros. assert (sameclass t x x). reflexivity. rewrite <- sameclass_equiv in H0. rewrite H0. discriminate. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)