proposition: Lemma syncE X X' : sync X X' -> match X with | (ts, ctx, t) => X' = many_app enc_halt_cbn [enc_list enc_eterm ts; enc_list enc_eterm ctx; enc_term t; enc_halt_cbn; I] end.
proof: Proof. by case. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect