tactics: descend into negative and "double negative" positions
tactics: descend into negative and "double negative" positions

We might get assertions we need to prove in positive, but not
strictly-positive, positions.

Consider

    val f : unit -> Pure int (req Phi) (ensures (fun x -> by_tactic tau (Psi x)))
    let f () = body

where body is inferred to have type

    Pure int wp'

the VC looks roughly like

    forall p. (forall x. (phi /\ (by_tactic tau (psi x)) ==> p x) ==> wp' p)

so psi, which the SMT (in most cases, I presume) try to prove should be
1) not wrapped with a by_tactic making it impossible to prove
2) simplified by the tactic engine

Also, we might get tactics on negative positions if they are in an
ensures clause of some definition. Like if we call the previously
defined `f`. In that case, we need to peel off the by_tactic to allow
the SMT solver to actually use that assumption.

This last one could also be fixed by a "irreducible but not abstract"
qualifier, but that does not exist.

A-Manning/FStar,FStarLang/FStar,FStarLang/FStar,A-Manning/FStar,FStarLang/FStar,A-Manning/FStar