Unfold lemmas for graft

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')
                                  end.

Resources

Solution