fact: Fixpoint step_bug (t : term) : option term := match t with | Const _ | Id _ => None | Abs x => None | App t1 t2 => if is_value t1 then match t1 with | Abs t => if is_value t2 then ret (subst 0 t1 t) else None | _ => None end else t1' <- step t1;; ret (App t1' t2) end.
imports: QuickChick(QuickChick) mathcomp(ssreflect ssrbool) String QuickChick.stlc(monad lambda)