fact: Fixpoint term_size (t : term) : nat := match t with | Const _ | Id _ => 1 | Abs t => 1 + (term_size t) | App t1 t2 => 1 + (term_size t1 + term_size t2) end.
imports: QuickChick(QuickChick) mathcomp(ssreflect ssrbool) String QuickChick.stlc(monad lambda)