fact: Definition type_eq_dec (t1 t2 : type) : {t1 = t2} + {t1 <> t2}.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia Program Relations Wellfounded Lexicographic_Product QuickChick(QuickChick) QuickChick.stlc(monad)