Rename `big_sep{L,L2,M,M2,S}_intuitionistically_forall` and `big_orL_lookup` to `big_*_intro`
also add wand_entails'
, which was used in some earlier version of these proofs
also add wand_entails'
, which was used in some earlier version of these proofs