proposition: Lemma l_subst_fpw : forall g s e l, lf' g (l_subst l s e) = lf' (fpw g s (af' g e)) l.
proof: Proof. intros g s e l; induction l; simpl; auto. rewrite subst_fpw; rewrite IHl; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom