proposition: Lemma inverse_union : forall R1 R2, inverse (union R1 R2) = union (inverse R1) (inverse R2).
proof: Proof. Proof using. unfold inverse, union. constructor; intros_all; dintuition eauto. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)