proposition: Lemma wf_lt_type : well_founded lt_type.
proof: Proof. unfold lt_type. apply wf_inverse_image. apply lt_wf. Qed.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia Program Relations Wellfounded Lexicographic_Product QuickChick(QuickChick) QuickChick.stlc(monad)