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