wp_apply/Texan triple improvements

wp_apply
could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib. 
wp_apply
could automatically try to prove that the expression is not a value, and then apply some variant ofwp_step
. This would remove the need to have a\later
in the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the nonvalue case). I think right now I regret that we decided for Texan triples to contain the\later
, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples. 
[More farfetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly
True
preconditions when the list is empty. 
When proving a triple, the postcondition could be wrapped in a fancy update, removing the need to
rewrite wp_fupd
in some of our proofs. Of course, when applying a triple, that update must not be in the way.
Blocked by #130