Contextual refinement

[dlesbre]

This is the output of my internship. For an extensive overview see my internship report on my website (report | slides)

For a brief summary of changes:

• Changes the definitions in linking.v, essentially gets rid of Main/Lib disjunction in favor of simply having a register
  state as a second argument to is_program or is_context.
• Add lemma on link well-formedness, associativity and commutativity and induction scheme.
• Add solve_can_link tactic to solve hypotheses that keep appearing in above lemmas.
• Adds contextual_refinement.v with a definition of CR and some results about it
• Adds contextual_refinement_adequacy.v which defines a new relation interp_exports relating exports of components
  and show some results relating this relation to rtc erased_step via adequacy. A large part of this comes from taking the results in examples/counter_binary_adequacy.v that don't depend on the counter.
• Change examples/counter_binary_adequacy.v to use the above abstractions
• Add files with results for stdpp fin map image and composition. I make merge requests for both to stdpp and the first one has been accepted but we should keep those files around until updating stdpp.
• Add some results in machine_run.v to show equivalence between exists n, machine_run _ _ = Some v and exists conf, rtc erased_step _ (v, conf)

Let me know if you think this is worth merging into main. Especially @ageorg29 since I changed your code quite a bit.