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