Generating triples and unconditional form for a DM4F effect

[kyoDralliam]

It would not be really difficult to have FStar generate for each DM4F effect MYEFFECT an effect

effect MyEffectTriple (a:Type) (pre: MYEFFECT.pre) (post: MYEFFECT.post a) =
  MYEFFECT a (fun x1 .. xn p -> pre x1 ... xn /\
            (forall y1 .. ym . pre x1 ... xn /\ post y1 ... ym ==> p y1 ... ym))

as well as

effect MyEffectNull (a:Type) =
  MYEFFECT a MYEFFECT.null_wp

The main "technical problem" to solve is how we give access to them after generation. Should we declare
new effects MYEFFECTTRIPLE and MYEFFECTNULL, or should we access them through MYEFFECT.Null/MYEFFECT.Triple (one caveat of this last approach is that MYEFFECT is not a namespace...)