include "Insert/inv.ma".
(* Functional properties ****************************************************)
-
+(*
theorem insert_total: \forall S,i,P. i <= P \to \exists Q. Insert S i P Q.
intros 4; elim H; clear H i P;
decompose; autobatch.
| lapply linear insert_inv_succ to H3; decompose; subst; autobatch
].
qed.
+*)