improve forward.destruct_it

[andrew-appel]

The following improvement to VST.floyd.forward.destruct_it unfolds type-definitions when looking for things to destruct:

Ltac destruct_it B :=
 match B with
 | ?C _ => destruct_it C
 | let '(x,y) := ?A in _ => destruct A as [x y]
 | match ?A with _ => _ end =>
    match type of A with ?tA => let uA := eval hnf in tA in  (* new *)
     match uA with
     | @sigT _ (fun x => _) => destruct A as [x A] 
     end end
 end.

For an example, see simple_cfem.verif_assemble.body_assemble_add.