module cotcr where -- Coinductive Soundness of Corecursive Type -- Class Resolution -- Contents: open import Intro open import Prelim open import IndRes --open import CoIndRes --open import ExtCoIndRes -- commit: 5fd8d3ee9d323cf87366b3c4f5a9377d6713deaf