我有这个目标，我想证明这一点。
1 goal
t1, t2 : FCPLang
H : evalS t1 = Some t2
______________________________________(1/1)
evalBS t1 = evalBS t2
为了证明这一点，我使用了induction t1.，但这些是引入的归纳假设：
1 goal
t1_1, t1_2, t1_3, t2 : FCPLang
H : evalS (if_then_else t1_1 t1_2 t1_3) = Some t2
IHt1_1 : evalS t1_1 = Some t2 -> evalBS t1_1 = evalBS t2
IHt1_2 : evalS t1_2 = Some t2 -> evalBS t1_2 = evalBS t2
IHt1_3 : evalS t1_3 = Some t2 -> evalBS t1_3 = evalBS t2
______________________________________(1/1)
evalBS (if_then_else t1_1 t1_2 t1_3) = evalBS t2
我认为这毫无用处，因为t2再次使用它们，而不是引入一个新术语，例如：
IHt1_1 : evalS t1_1 = Some t2_1 -> evalBS t1_1 = evalBS t2_1
我该如何解决这个问题？