proposition: Lemma eq_can_extr : forall (s si : skel) (X Y : Can s), eq_can s X Y -> eq_can si (coerce_CR si (iK s X)) (coerce_CR si (iK s Y)).
proof: Proof. unfold coerce_CR in |- *. intros. elim (EQ_skel s si); auto with coc core arith datatypes. intro Heq; case Heq; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can