(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/".
+
include "logic/equality.ma".
include "nat/nat.ma".
axiom jmcBA : ∀n,m.∀p:A n = B m.B m -> A n.
axiom jmcAB : ∀n,m.∀p:A n = B m.A n -> B m.
-coercion cic:/matita/test/jmcAB.con.
-coercion cic:/matita/test/jmcBA.con.
+coercion cic:/matita/tests/coercions_open/jmcAB.con.
+coercion cic:/matita/tests/coercions_open/jmcBA.con.
axiom daemon : ∀x,y:A O.x = y.
alias num (instance 0) = "natural number".
lemma xx : ∀b:B 2.∀a:A 1.eatA ? b = eatB ? a.
intros; [3,5,7,9: apply AB|1: apply daemon];skip.
-qed.
\ No newline at end of file
+qed.