• Dan Frumin's avatar
    Make some lemmas and tactics lamsubst-aware · 3c36b147
    Dan Frumin authored
    - Twiggle with the burden of proof in log_related_arrow
    - rel_rec_l/r returns a goal with an (unsimplified) lamsubst
      and can detect locked lambdas
    - Fix some notational issues [hax.v]
    - Rewrite the counter refinement proof to make greater use of lamsubst
    3c36b147
lateearlychoice.v 7.38 KB