proposition: Lemma ren_many_app xi M Ns : ren xi (many_app M Ns) = many_app (ren xi M) (map (ren xi) Ns).
proof: Proof. elim: Ns M; [done|]. move=> > IH ? /=. by rewrite IH. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect