proposition: Lemma closed_I s : (forall k, L.subst s k (lam (var 0)) = s) -> L.closed s.
proof: Proof. move=> H k u. elim: s k u {H}(H k). - move=> /=. move=> n k u. by case: (Nat.eqb n k). - by move=> ? IH1 ? IH2 k ? /= [/IH1 -> /IH2 ->]. - by move=> ? IH k ? /= [/IH ->]. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect