fact: Definition decompose_forallT : forall {B : Type -> Type} (T : Type) (success : forall (A : Type) (b : A -> Type), t (B (forall a : A, b a))) (failure : t (B T)), t (B T).
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)