proposition: Lemma trans : forall a b x, create (create x a) b = create x (fun y=> b (a y)).
proof: Proof. ir. ap extensionality; uhg; ir. rwi inc_rw H. nin H; ee. rw inc_rw. rwi inc_rw H. nin H; ee. sh x2. ee; try am. rw H1; am. rwi inc_rw H. nin H; ee. rw inc_rw. sh (a x1); ee. rw inc_rw. sh x1; ee; try tv. am. Qed.
imports: tactics