proposition: Lemma a_subst_fpw : forall m a x e g, i_a m g (a_subst a x e) = i_a m (fpw g x (af' g e)) a.
proof: Proof. intros m' a x e g; induction a; simpl. destruct b as [e1 e2]; simpl. do 2 rewrite subst_fpw; auto. rewrite IHa; auto. rewrite IHa1; rewrite IHa2; auto. induction m'; auto. simpl. destruct a as [ps p]; destruct (string_dec ps s); simpl; auto. rewrite l_subst_fpw; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom