〈0,1〉 ≃ 〈1,2〉. Unfolding the notation, that corresponds to
eqrel ? (eq_setoid ?) 〈0,1〉 〈1,2〉 which means that the two
pairs are to be compare according to the equivalence relation
〈0,1〉 ≃ 〈1,2〉. Unfolding the notation, that corresponds to
eqrel ? (eq_setoid ?) 〈0,1〉 〈1,2〉 which means that the two
pairs are to be compare according to the equivalence relation