proposition: Lemma Krivine_step_eclosed ts ctx t ts' ctx' t' : Krivine_step (ts, ctx, t) (ts', ctx', t') -> Forall eclosed ts -> eclosed (closure ctx t) -> Forall eclosed ts' /\ eclosed (closure ctx' t').
proof: Proof. move EX: (ts, ctx, t) => X. move EY: (ts', ctx', t') => Y H. case: H EX EY=> > [-> -> ->] [-> -> ->] /=. - tauto. - move=> ? [/boundE] *. split; [done|split; [apply: dclvar; lia|tauto]]. - move=> ? [/boundE] ??. split; [|tauto]. constructor; cbn; tauto. - move=> /Forall_cons_iff ? [/boundE]. tauto. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect