Generalize Equiv_ctx to source programs that may not be safe,
by proving that Compositional CompCert implies behavior refinement:
  If linked C[prog2] diverges, then C[prog1] diverges or goes wrong.
  If linked C[prog2] terminates, then C[prog1] terminates or goes wrong.
Proof currently uses excluded middle but this can be fixed.
This notion of program refinement is a preorder (reflexive and transitive).