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 Arith Lia Dblib(DblibTactics DeBruijn)