proposition: Lemma lem_small_to_big_aux : forall p p', p --> p' -> forall c1 s1 c2 s2 s, p = (c1, s1) -> p' = (c2, s2) -> c2 >> s2 ==> s -> c1 >> s1 ==> s.
proof: Proof. time (induction 1; sauto). Undo. time (induction 1; sauto l: on). Undo. time (induction 1; sauto lq: on). Qed.
imports: Hammer(Tactics Reflect) String Arith Lia Relations