proposition: Lemma step_ext: forall s1 s3 l s2 s4, step s1 l s2 -> (forall n, s1 n = s3 n) -> (forall n, s2 n = s4 n) -> step s3 l s4.
proof: Proof. Proof using. intros s1 s3 l s2 s4 Hstep Heq1 Heq2. apply functional_extensionality in Heq1. apply functional_extensionality in Heq2. subst; auto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)