proposition: Lemma length_insert_general: forall A x k o (e : env A), length e = k -> length (raw_insert x o e) = mymax (1 + k) (1 + x).
proof: Proof. induction x; simpl; intros; subst. mymax. destruct e; simpl. mymax. erewrite IHx by reflexivity. simpl. mymax. erewrite IHx by reflexivity. mymax. Qed.
imports: List Dblib(DblibTactics DeBruijn)