proposition: Lemma loop_injective k1 k2 a b b' : loop a k1 = Some b -> loop a k2 = Some b' -> b = b'.
proof: Proof. revert k2 b b' a. induction k1; intros; cbn in *. - destruct (p a) eqn:E; inv H. destruct k2; cbn in H0; rewrite E in H0; now inv H0. - destruct (p a) eqn:E. + inv H. destruct k2; cbn in H0; rewrite E in H0; now inv H0. + destruct k2; cbn in H0; rewrite E in H0; try now inv H0. eauto. 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