Can I safely assume that isomorphic types are equal?

These kind of questions are the domain of predilection of homotopy type theory but here is a tentative synthetic answer to your questions.

In CIC (± the ideal theory underlying Coq), we say that two types A and B are equivalent if there is a function f : A -> B with left inverse g : B -> A (that is f o g = id_B) and right inverse h : B -> A (that is h o f = id_B). You can use an isomorphism from A to B to show that they are equivalent. Homotopy type theory is concerned with the addition of an axiom to CIC (or rather MLTT) called univalence that roughly states that equivalence between types and equality coincide (to be more precise, there is a map id_to_equiv : A = B -> equiv A B and univalence says that this map is itself an equivalence). Univalence is compatible with CIC in the sense that there exist models of CIC that validate this axiom.

So to answer your questions:

1. Yes, one cannot prove A <> B in CIC because any such proof would contradict univalence (hence no model of CIC + univalence could exist)
2. You won't be able to prove False since it is a special case of univalence that does have models, however the computational content of Coq will be partially lost (as it is always the case with the addition of any axiom).
3. Univalence is compatible with some axioms of the standard library of Coq (excluded-middle for instance) but not with others (Uniqueness of identity proofs, a.k.a. UIP, univalence states that there are 2 proofs of Bool = Bool). Concerning the absence of univalence from the standard library, it stems from the fact that the standard library defines equality in Prop, which is incompatible with the existence of multiple witnesses of identity. However the axiom that you mention might be formulated in a way that's compatible with UIP (there have been some work by Bauer and Winterhalter on a so called cardinal model of type theory). Whether it is compatible with the other axioms from the standard library would have to be checked.