Theory ArityEtaExpansionSafe

theory ArityEtaExpansionSafe
imports EtaExpansionSafe ArityStack ArityEtaExpansion
begin

lemma Aeta_expand_safe:
  assumes "Astack S ⊑ a"
  shows "(Γ, Aeta_expand a e, S) ⇒⇧* (Γ, 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_safe')
qed


end