open import Level open import Chapter4.Desc open import Chapter4.Desc.Fixpoint open import Chapter4.Desc.Lifting open import Chapter4.Desc.Induction module Chapter7.Case {ℓ k : Level} (D : Desc ℓ) (P : μ D → Set (ℓ ⊔ k)) where case : ((xs : ⟦ D ⟧ (μ D)) → P ⟨ xs ⟩) → (x : μ D) → P x case cases = induction {k = k} D P (λ {xs} _ → cases xs)