Weaken the associativity axiom of the Dra class.

Now, associativity needs only to be established in case the elements are
valid and their compositions are defined. This is very much like the notion
of separation algebras I had in my PhD thesis (Def 4.2.1). The Dra to Ra
construction still easily works out.
4 jobs for master in 8 minutes and 55 seconds
Status Job ID Name Coverage
  Build
passed #4301
fp-timing
build-coq.8.6.1

00:08:37

passed #4300
fp-timing
build-coq.8.7

00:02:39

 
  Deploy
passed #4302
opam

00:00:16

passed #4303
reverse-deps

00:00:14