fact: Definition fix2 : forall {A1: Type} {A2: A1->Type} (B: forall (a1 : A1), A2 a1->Type), ((forall (x1: A1) (x2: A2 x1), t (B x1 x2)) -> (forall (x1: A1) (x2: A2 x1), t (B x1 x2))) -> forall (x1: A1) (x2: A2 x1), t (B x1 x2).
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)