proposition: Lemma sameclass_equiv' : forall `{WF} y z, sameclass t y z -> forall x, @fst bool UF (equiv t y x) = fst (equiv t z x).
proof: Proof. intros t Hwf y z H. intros. apply <- bool_prop_iff. rewrite 2 sameclass_equiv. rewrite H. reflexivity. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)