fact: Fixpoint step (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 t2' <- step t2;; ret (App t1 t2') | _ => None end else t1' <- step t1;; ret (App t1' t2) end.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia Program Relations Wellfounded Lexicographic_Product QuickChick(QuickChick) QuickChick.stlc(monad)