今天 WC 上午第一课堂，但是有个题不会做。。。

Lemma left_most_reverse: forall t default,
  left_most (tree_reverse t) default = right_most t default.
Proof.
  intros.
  induction t; simpl.
  - reflexivity.
  - (** 然后不会了 /kk *)
Admitted. (* 留作习题 *)

遇到的问题：归纳的变量不同不能直接 rewrite

1 goal
t1 : tree
v : Z
t2 : tree
default : Z
IHt1 : left_most (tree_reverse t1) default = right_most t1 default
IHt2 : left_most (tree_reverse t2) default = right_most t2 default
______________________________________(1/1)
left_most (tree_reverse t2) v = right_most t2 v

完整代码

求教了