proposition: Lemma lem_while_cong_aux : forall b c c' s s', While b Do c >> s ==> s' -> c ~~ c' -> While b Do c' >> s ==> s'.
proof: Proof. intros *. remember (While b Do c). induction 1; sauto lq: on unfold: equiv_cmd. Qed.
imports: Hammer(Tactics Reflect) String Arith Lia