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