Tree Identities in Coq

Tree.v

Require Import List.

Inductive btree : Set :=
 | bleaf : btree
 | bbranch : btree -> btree -> btree.

Fixpoint btree_id(x : btree) : btree :=
 match x with
  | bleaf => bleaf
  | bbranch l r => bbranch (btree_id l) (btree_id r)
 end.

Theorem btree_id_is_id: forall b, btree_id(b) = b.
Proof.
intros.
induction b.
 simpl.
 reflexivity.
 
 simpl.
 f_equal.
  assumption.
  assumption.
Qed.
  
Inductive mtree : Set :=
 | mleaf : mtree
 | mbranch : list mtree -> mtree.

Fixpoint mtree_id(x : mtree) : mtree :=
 match x with
  | mleaf => mleaf
  | mbranch xs => mbranch (map mtree_id xs) 
 end.


Theorem mtree_id_is_id: forall m, mtree_id(m) = m.