+ [ exact (C r)
+ | rewrite > (with_ r); exact (mult (r2_ r))]
+qed.
+coercion cic:/matita/tests/multiple_inheritance/r2.con.
+
+(* convertibility test *)
+lemma conv_test : ∀r:R.C r -> K r.
+ intros.
+ change with (C (r1 r)).
+ change with (K (r2 r)).
+ change with (C (r1 r)).
+ assumption.