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