proposition: Lemma widen2_top_rec : forall e l g, i_a Ab.m g (to_a1 (widen2 e) l).
proof: Proof. induction e; intros l g; simpl. i_a_to_to_p. apply Ab.bot_semantics. destruct a as [s p]; simpl; destruct (str_in_list s l); simpl; auto. destruct (to_syn bot). split; auto. i_a_to_to_p. apply Ab.bot_semantics. Qed.
imports: syntax little denot Bool List String ZArith axiom