fact: Definition lt_type (tau1 tau2 : type) : Prop := type_size tau1 < type_size tau2.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia Program Relations Wellfounded Lexicographic_Product QuickChick(QuickChick) QuickChick.stlc(monad)