proposition: Lemma Krivine_step_dec X : (exists Y, Krivine_step X Y) \/ (stuck Krivine_step X).
proof: Proof. move: X => [[ts ctx] t]. move: t => [[|?]|??|?]. - move: ctx => [|[??]?]. + right. move=> ? H. by inversion H. + left. eexists. by constructor. - move: ctx=> [|??]. + right. move=> ? H. by inversion H. + left. eexists. by constructor. - left. eexists. by constructor. - move: ts => [|??]. + right. move=> ? H. by inversion H. + left. eexists. by constructor. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect