proposition: Lemma subst_closed {sigma t} : L.closed t -> subst sigma t = t.
proof: Proof. move=> /closed_dcl /bound_ext_subst_term. rewrite -[RHS]subst_var_term. apply. lia. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect