proposition: Lemma to_assert_bot : forall e g, i_a m g (to_assert bot e).
proof: Proof. intros e g; unfold to_assert. case_eq (to_syn bot); intros ts l Hts; simpl. rewrite f_p_lookup. rewrite lf'_app; rewrite lf_lz_to_a; simpl. rewrite <- to_syn_ok with (1:=Hts); auto. apply Ab.bot_semantics. Qed.
imports: syntax little denot Bool List String ZArith axiom