fact: Definition preservation_derived (e : term) (t: type) : Checker := match step e with | Some e' => checker (typing nil e' t ?? 10) | None => checker true end.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia QuickChick(QuickChick)