From dbac63ed42caf9e5edaf1f1007700535f2a7c923 Mon Sep 17 00:00:00 2001
From: h7x4 <h7x4@nani.wtf>
Date: Thu, 25 Jun 2026 23:23:35 +0900
Subject: [PATCH] chap5: improve `fv_leq_size` slightly

---
 src/chap5.v | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/src/chap5.v b/src/chap5.v
index 68af317..e36c92d 100644
--- a/src/chap5.v
+++ b/src/chap5.v
@@ -371,17 +371,14 @@ Module Chap5.
     induction t as [x | x body IH | t1 IH1 t2 IH2].
     - simpl. reflexivity.
     - simpl.
-      assert (H : length (set_remove string_dec x (free_vars body)) <= length (free_vars body)).
-      { apply set_remove_length_le. }
-      rewrite H.
-      assert (H2 : length (free_vars body) <= size body).
-      { apply IH. }
-      rewrite H2.
+      transitivity (length (free_vars body)).
+      apply set_remove_length_le.
+      transitivity (size body).
+      apply IH.
       apply Nat.le_succ_diag_r.
     - simpl.
-      assert (H1: length (set_union string_dec (free_vars t1) (free_vars t2)) <= length (free_vars t1) + length (free_vars t2)).
-      { apply set_union_length_le. }
-      rewrite H1.
+      transitivity (length (free_vars t1) + length (free_vars t2)).
+      apply set_union_length_le.
       apply le_sum.
       + apply IH1.
       + apply IH2.