theory ArityEtaExpansionSestoft
imports EtaExpansionSestoft ArityStack EtaExpansionArity
begin
lemma Aeta_expand_correct:
assumes "Astack S \ a"
shows "(\, Aeta_expand a e, S) \\<^sup>* (\, e, S)"
proof-
have "arg_prefix S = Rep_Arity (Astack S)"
by (induction S arbitrary: a rule: arg_prefix.induct) (auto simp add: Arity.zero_Arity.rep_eq[symmetric])
also
from assms
have "Rep_Arity a \ Rep_Arity (Astack S)" by (metis below_Arity.rep_eq)
finally
show ?thesis
by transfer (rule eta_expansion_correct')
qed
end