Use is_true in refinement_common.
Flip argument order to help unification.
Use and4 in cache_correct.
Adapt existT injectivity lemma to eqType.
Start splitting SERVICE from other opcodes.
Remove intermediate decoding step, inversion lemma
Fix more rule definitions.
Bring back proof of analyze_cache.