fact: Definition fix1 : forall{A: Type} (B: A->Type), ((forall x: A, t (B x))->(forall x: A, t (B x))) -> forall x: A, t (B x).
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)