proposition: Lemma lem_unfold_while : forall b c, While b Do c ~~ If b Then c;; While b Do c Else Nop.
proof: Proof. sauto l: on unfold: equiv_cmd. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String