experiment with dependent squashing...

comment out unfinished proofs