proposition: Lemma flatten_var_0 t ctx : flatten (closure (t :: ctx) (var 0)) = flatten t.
proof: Proof. move: t => [? ?] /=. rewrite !simpl_term /=. apply: ext_subst_term => ?. by rewrite !simpl_term. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect