Theory ArityAnalysisFixProps

theory ArityAnalysisFixProps
imports ArityAnalysisFix ArityAnalysisSpec
begin

context SubstArityAnalysis
begin

lemma Afix_restr_subst:
  assumes "x ∉ S"
  assumes "y ∉ S"
  assumes "domA Γ ⊆ S"
  shows "Afix Γ[x::h=y]⋅ae f|` S = Afix Γ⋅(ae f|` S) f|` S"
  by (rule Afix_restr_subst'[OF Aexp_subst_restr[OF assms(1,2)] assms])
end


end