update

Author: Koukyosyumei

Loda/Test/CommandTest.lean

@@ -22,8 +22,7 @@ open Env
               Ast.IntegerOp.add (Ast.Expr.constBool True) (Ast.Expr.constBool True) hΓ hΓ
   obtain ⟨vv, hv_eq⟩ := int_refintype_implies_exists_int_value 1000 σ Δ Γ "x" (Expr.constBool True) hΓ hσ
   have h_sub := two_mul_I 1000 σ Δ Γ "x" vv hv_eq
-  simp [h_delta, Γ, Ast.v] at h_sub
-  simp [h_delta, Ast.v] at h_body
+  simp [h_delta, Γ, Ast.v] at h_sub h_body
   exact Ty.TypeJudgment.TE_SUB h_sub h_body
 }