proposition: Lemma loop_monotone (k1 k2 : nat) (a b : A) : loop a k1 = Some b -> k1 <= k2 -> loop a k2 = Some b.
proof: Proof. revert a k2; induction k1 as [ | k1' IH]; intros a k2 HLoop Hk; cbn in *. - destruct k2; cbn; destruct (p a); now inv HLoop. - destruct (p a) eqn:E. + inv HLoop. now apply loop_0. + destruct k2 as [ | k2']; cbn in *; rewrite E. * exfalso. lia. * apply IH; [assumption|lia]. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes Undecidability.Shared.Libs.PSL.FiniteTypes.BasicFinTypes Undecidability.Shared.Libs.PSL.FiniteTypes.CompoundFinTypes Undecidability.Shared.Libs.PSL.FiniteTypes.VectorFin Undecidability.Shared.Libs.PSL.Vectors.FinNotation Undecidability.Shared.Libs.PSL.Inhabited Undecidability.Shared.Libs.PSL.Base Undecidability.Shared.Libs.PSL.Vectors.Vectors Lia