Derive lifting axioms for ectx languages

This required a new ectx axiom: Positivity of evaluation contexts. This axiom was
also present in the old Iris 1.1 development, back when it still derived lifting
axioms for ectx languages.
1 job for master
Status Job ID Name Coverage
  Test
passed #308
coq
buildjob

00:03:20