proposition: Lemma Eta (s : term ) t : closed s -> lambda t -> app (lam (app s #0)) t == app s t.
proof: Proof. intros cls_s lam_t. eapply star_equiv, starC; eauto using step_Lproc. simpl. rewrite cls_s. reflexivity. Qed.
imports: Lia