proposition: Lemma interp_equiv rho c : C.interp rho c = interp_uf rho c.
proof: Proof. induction c as [ |l c IHc]; simpl; auto. rewrite IHc. destruct c as [ |l' c]; simpl; auto. now rewrite orb_false_r. Qed.
imports: State SMT_terms List Bool PArray Int63