proposition: Lemma fold_invariant: forall A B (P : env A -> B -> Prop) f accu, P (@empty _) accu -> (forall o e accu, P e accu -> P (raw_insert 0 o e) (f o accu)) -> forall e, P e (fold f e accu).
proof: Proof. intros ? ? ? ? ? init step. induction e; simpl. - eapply init. - eapply step. eauto. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)