proposition: Lemma hinit_inside: forall h sz l l', l <= l' < l + Z.of_nat sz -> hinit l sz h l' = Some 0.
proof: Proof. induction sz; intros; cbn. - lia. - destruct (Z.eq_dec l l'); auto. apply IHsz. lia. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)