proposition: Lemma to_syn_ok : forall v x s l p, to_syn v = (s,l) -> syntax.lookup string_dec m (fun l => True) s = p -> to_p v x = p (l++x::nil).
proof: Proof. unfold to_syn, m; intros [[lb | | ][ub | | ]] x s l p H; injection H; intros Hl Hs; subst s l; simpl; repeat decide_strings; intros Hp; subst p; simpl; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom