(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/overred/".
+
include "logic/equality.ma".
axiom t3 : T3.
axiom c : T2 -> X -> X.
-coercion cic:/matita/test/overred/c.con 1.
+coercion cic:/matita/tests/overred/c.con 1.
axiom daemon : c t3 x = x.
theorem find_a_coercion_from_T2_for_a_term_in_T3 : (* c *) t3 x = x.
apply daemon.
-qed.
\ No newline at end of file
+qed.