proposition: Lemma thinner_env_to_a1 : forall l1 l2, thinner_env l1 l2 -> forall g l, i_a Ab.m g (to_a1 l1 l) -> i_a Ab.m g (to_a1 l2 l).
proof: Proof. induction 1; intros g l; simpl. auto. case (str_in_list s l). auto. destruct (to_syn i1); destruct (to_syn i2). simpl; intros [H' H'']; split; auto. i_a_to_to_p. apply Ab.thinner_prop with (1:= H); auto. to_p_to_i_a; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom