proposition: Lemma gen_term_size_eq (e : env) (p : nat * type) : gen_term_size p e = gen_term_size_unfold p e.
proof: Proof. unfold_sub gen_term_size (gen_term_size p e); simpl. destruct p as [[|n] [|]]; try reflexivity; destruct (vars_with_type e _) eqn:Heq; simpl; repeat (rewrite !Heq /=; apply f_equal; try reflexivity). Qed.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia Program Relations Wellfounded Lexicographic_Product QuickChick(QuickChick) QuickChick.stlc(monad)