proposition: Lemma flatten_var_S t ctx n : flatten (closure (t :: ctx) (var (S n))) = flatten (closure ctx (var n)).
proof: Proof. done. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect