Solved WHILE_false_informal.
Solved WHILE_true_nonterm_informal
Solved WHILE_true.
Solved seq_assoc.
Solved assign_aequiv.