fact: Definition prop_preservation_derived_checker := forAll (@arbitrary type _) (fun t => forAll (gen_typed 5 nil t) (fun e => preservation_derived e t)).
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia QuickChick(QuickChick)