Test if-statement syntax and semantics

[cowang]

Write a Cucumber feature with the if-then- and if-then-else syntax and semantics

• allow either blocks or individual statements that are interpreted as trivial blocks
• show an if-then statement whose proof fails because an assigned value in the then-block isn't dealt with when the condition is false
• show how we need a trivial assignment, which is ignored in implementation, where we would normally use an if-then statement
• mention that an if-then statement might be useful for non-tracked state-change, such as logging
• show several equivalent ways to interpret an if-then-else in a means-statement

Semantics

A natural semantics for the if-then-else-statement is
(Condition -> Then-semantics) /\ (~Condition -> Else-semantics) but use the equivalent
(Condition /\ Then-semantics) \/ (~Condition /\ Else-semantics) to reduce the number of disjunctions, since implication is implicitly a disjunction.

[cowang]

Leaving this open because the merged branch "Accept if statement" #18 does not completely handle proofs. Need to handle blocks correctly before this can be done.