/*@ axiomatic Inj {
   axiom inj1: \true;
   axiom inj1: \true;
}
*/