proposition: Lemma liftPhi_correct Vars: (forall s, s el Vars -> proc s) -> Proc (liftPhi Vars).
proof: Proof. intros H n. unfold liftPhi. destruct (nth_in_or_default n Vars I) as [?|eq]. - now apply H. - rewrite eq. cbv. split. auto. eexists. eauto. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd