proposition: Lemma tag_eqP : Equality.axiom tag_eq.
proof: Proof. rewrite /tag_eq => [] [i x] [j] /=. case: eqP => [<-|Hij] y; last by right; case. by apply: (iffP eqP) => [->|<-]; rewrite tagged_asE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)