proposition: Fact df_ren_size ρ f : df_size f⦃ρ⦄ = df_size f.
proof: Proof. revert ρ; induction f; intros; simpl; auto; do 2 f_equal; auto. Qed.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)