proposition: Lemma loop_unlift (k : nat) (a : A) (b' : B) : loop f' h' (lift a) k = Some b' -> exists a' : A, loop f h a k = Some a' /\ b' = lift a'.
proof: Proof. Proof using halt_lift_comp step_lift_comp. revert a b'. induction k as [ | k']; intros; cbn in *. - rewrite halt_lift_comp in H. exists a. destruct (h a) eqn:E; now inv H. - rewrite halt_lift_comp in H. destruct (h a) eqn:E. + exists a. now inv H. + rewrite step_lift_comp in H by assumption. specialize IHk' with (1 := H) as (x&IH&->). now exists x. 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