Grafting trees

Define the function graft such that (graft t t') is the tree obtained by replacing all leaves of t by t'.
prove the following unfolding lemmas:

Lemma graft_unfold1 {A: Type}: forall t': LTree A, graft LLeaf  t' = t'.

Lemma graft_unfold2 {A: Type}: forall (a:A) (t1 t2 t':LTree A),
                      (graft (LBin a t1 t2) t')=
                      (LBin a (graft t1 t') (graft t2 t')).

Lemma graft_unfold {A: Type}: forall  (t t': LTree A),
                     graft t t' = match t  with
                                  | LLeaf => t'
                                  | LBin n t1 t2 =>
                                             LBin  n (graft t1 t')
                                                     (graft t2 t')
                                  end.

Resources
You must load the solution  of 
this exercise.

 Solution 
 Follow this link