fact: Fixpoint step (e : term) : option term := match e with | Const _ | Id _ => None | Abs _ x => None | App (Abs t e1) e2 => if is_value e2 then Some (subst 0 e2 e1) else match step e2 with | Some e2' => Some (App (Abs t e1) e2') | None => None end | App e1 e2 => match step e1 with | Some e1' => Some (App e1' e2) | None => None end end.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia QuickChick(QuickChick)