proposition: Theorem lookup_update_eq : forall (n:nat) (s s':state) (v:Z), update s n v = Some s' -> lookup n s' = Some v.
proof: Proof. simple induction n. - intros s; case s. + intros; discriminate. + simpl in |- *; intros z tl s' v Heq; injection Heq; intros Heq1; rewrite <- Heq1; trivial. - intros p Hrec s; case s; simpl in |- *; try (intros; discriminate). intros z l s' v; generalize (fun s':state => Hrec l s' v). case (update l p v); simpl in |- *; try (intros; discriminate). intros s'0 Hrec' Heq; injection Heq; intros Heq1; rewrite <- Heq1; simpl in |- *; rewrite Hrec'; auto. Qed.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction List Arith Compare_dec Lia