fact: Definition coerce_CR (s : skel) (i : Int_K) : Can s := match i with | iK si Ci => match EQ_skel si s with | left y => match y in (_ = x) return (Can x) with | refl_equal => Ci end | _ => default_can s end | _ => default_can s end.
imports: Termes Conv Types Class Can