fact: Definition preservation_prop (c : term -> type -> Checker) := forAll (@arbitrary type _) (fun t => forAllMaybe ((genST (fun e => typing nil e t))) (fun e => c e t)).
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia QuickChick(QuickChick)