proposition: Lemma l_subst_app : forall l1 l2 x e', l_subst (l1++l2) x e' = l_subst l1 x e' ++ l_subst l2 x e'.
proof: Proof. intros l1 l2 x e'; induction l1; simpl; auto. rewrite IHl1; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom