Inductive tree : Set := | leaf : nat -> tree | node : tree -> nat -> tree -> tree. Fixpoint mirror (T : tree) : tree := match T with | leaf n => leaf n | node T1 n T2 => node (mirror T2) n (mirror T1) end. Fixpoint map (f : (nat -> nat)) (T : tree) : tree := match T with | leaf n => leaf (f n) | node T1 n T2 => node (map f T1) (f n) (map f T2) end. Theorem mapmirror : forall T : tree, forall f : nat -> nat, map f (mirror T) = mirror (map f T). Proof. intros. induction T. simpl. reflexivity. simpl. rewrite <- IHT1. rewrite IHT2. reflexivity. Qed.