fact: Definition rev_injective_checker : Checker := forAll (genST (fun l1l2 => equal_reverses l1l2)) (fun l1l2 => match l1l2 with | Some (Coq.Init.Datatypes.pair l1 l2) => ((l1 = l2)?) | None => true end).
imports: QuickChick(QuickChick) List ZArith Induction