+coercion cic:/matita/logic/equality/eq_f.con.
+coercion cic:/matita/logic/equality/eq_f1.con.
+variant xxx : ? \def eq_f.
+coercion cic:/matita/tests/coercions/xxx.con.
+
+theorem coercion_svelta : \forall T,S:Type.\forall f:T \to S.\forall x,y:T.x=y \to f y = f x.
+ intros.
+ apply ((\lambda h:f y = f x.h) H).
+qed.
+
+variant pos2nat' : ? \def pos2nat.
+
+coercion cic:/matita/tests/coercions/xxx.con.
+
+inductive initial: Set \def iii : initial.
+
+definition i2pos: ? \def \lambda x:initial.one.
+
+coercion cic:/matita/tests/coercions/i2pos.con.
+
+coercion cic:/matita/tests/coercions/pos2nat'.con.
+
+