Unfold lemmas for graft

You've defined a graft operation in this exercise .
You're asked to prove unfold lemmas, i.e. the following theorems :
Lemma graft_unfold1 : forall (A:Set) (t': LTree A), graft LLeaf  t' = t'.

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

Lemma graft_unfold : forall (A:Set) (t t': LTree A),
                     graft t t' = match t  with
                                  | LLeaf => t'
                                  | LBin n t1 t2 =>
                                             LBin  n (graft t1 t')
                                                     (graft t2 t')


Load This file


Follow this link for a complete solution.

Going home
Pierre Castéran