+ rewrite mapOptionTree_compose.
+ rewrite pf2.
+ replace ((mapOptionTree unlev (y @@@ t))) with y.
+ apply X0.
+ clear pf1 X0 X1 pfdist pf2 vars varstypes.
+ induction y; try destruct a; auto.
+ rewrite IHy1 at 1.
+ rewrite IHy2 at 1.
+ reflexivity.