proposition: Lemma extr_eq : forall (P : forall s : skel, Can s -> Prop) (s : skel) (c : Can s), P s c -> P s (coerce_CR s (iK s c)).
proof: Proof. intros. unfold coerce_CR in |- *. elim (EQ_skel s s). intro Heq. change ((fun s0 (e : s = s0) => P s0 match e in (_ = x) return (Can x) with | refl_equal => c end) s Heq) in |- *. case Heq; trivial. simple induction 1; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can