proposition: Lemma TaggedP (T1 : Type) (T2 : T1 -> Type) (P : forall x, T2 x -> Type) : (forall t : {x : T1 & T2 x}, P _ (tagged t)) -> forall (x : T1) (y : T2 x), P x y.
proof: Proof. by move=> /(_ (Tagged _ _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)