Skip to content

Rename `big_sep{L,L2,M,M2,S}_intuitionistically_forall` and `big_orL_lookup` to `big_*_intro`

Ralf Jung requested to merge ralf/big-sep-intro into master

also add wand_entails', which was used in some earlier version of these proofs

Merge request reports