fact: Fixpoint show_type (tau : type) := match tau with | N => "Nat" | Arrow tau1 tau2 => "(" ++ show_type tau1 ++ " -> " ++ show_type tau2 ++ ")" end.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia Program Relations Wellfounded Lexicographic_Product QuickChick(QuickChick) QuickChick.stlc(monad)