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