proposition: Lemma hupdate_other: forall l v h l', l <> l' -> (hupdate l v h) l' = h l'.
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)