theorem insert_inv_zero: \forall S,P,Q. Insert S zero P Q \to Q = abst P S.
intros; inversion H; clear H; intros; subst; autobatch.
qed.
theorem insert_inv_zero: \forall S,P,Q. Insert S zero P Q \to Q = abst P S.
intros; inversion H; clear H; intros; subst; autobatch.
qed.