proposition: Lemma hupdate_same: forall l v h, (hupdate l v h) l = Some v.
proof: Proof. intros; cbn. destruct (Z.eq_dec l l); congruence. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)