proposition: Lemma lem_unfold_while : forall b c, While b Do c ~~ If b Then c;; While b Do c Else Nop.
proof: Proof. time sauto unfold: equiv_cmd. Undo. time sauto q: on unfold: equiv_cmd. Undo. time sauto l: on unfold: equiv_cmd. Qed.
imports: Hammer(Tactics Reflect) String Arith Lia