proposition: Lemma is_can_coerce : forall s s' C, is_can s C -> is_can s' (coerce_CR s' (iK s C)).
proof: Proof. simpl in |- *; intros. elim (EQ_skel s s'); intros; auto with coc. case a; trivial. Qed.
imports: Termes Conv Types Class Can