proposition: Lemma subst_to_assert : forall v e x e', a_subst (to_assert v e) x e' = to_assert v (subst e x e').
proof: Proof. intros v e x e'; unfold to_assert; destruct (to_syn v) as [p l]. simpl; rewrite l_subst_app; rewrite l_subst_lz_to_a; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom