Generating `triples` and `unconditional` form for a DM4F effect

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...)

Start by reviewing the DM4F effect-generation path and the MYEFFECT, MYEFFECT.pre, MYEFFECT.post, and MYEFFECT.null_wp definitions named in the issue. Determine how generated MyEffectTriple and MyEffectNull effects should be exposed, then verify that generation produces both forms with the intended access convention.

Written by the indexing model from the issue text.