proposition: Lemma injective_inverse : injective (@inverse A).
proof: Proof. Proof using. intros R1 R2 E. extens. intros x y. unfolds inverse. rewrite* (fun_eq_2 y x E). Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)