chap5: improve fv_leq_size slightly

2026-06-25 23:23:35 +09:00
parent 28c71cf03f
commit dbac63ed42
1 changed files with 6 additions and 9 deletions
@@ -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.