proposition: Lemma halt_cbnE ts ctx u : halt_cbn ts ctx u -> match u with | var 0 => match ctx with | [] => False | (closure ctx' t')::_ => halt_cbn ts ctx' t' end | var (S n) => match ctx with | [] => False | _::ctx' => halt_cbn ts ctx' (var n) end | app s t => halt_cbn ((closure ctx t) :: ts) ctx s | lam s => match ts with | [] => True | t'::ts' => halt_cbn ts' (t'::ctx) s end end.
proof: Proof. by case. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect