proposition: Lemma thinner_env_prop_rec : forall l l', thinner_env l l' -> forall g ig, i_a Ab.m g (to_a1 l ig) ->i_a Ab.m g (to_a1 l' ig).
proof: Proof. intros l l'; induction 1; intros g ig Hl; simpl in Hl |- *; auto. destruct (str_in_list s ig). auto. destruct (to_syn i1); destruct (to_syn i2); split; simpl in Hl; destruct Hl as [H1 H2]; auto. unfold to_assert in *. case_eq (to_syn i1); intros ps1 l1 Hts1. case_eq (to_syn i2); intros ps2 l2 Hts2. generalize H1; clear H1. rewrite Hts1. simpl; repeat rewrite lf'_app; repeat rewrite lf_lz_to_a; simpl. repeat rewrite f_p_lookup. rewrite <- to_syn_ok with (1:=Hts1); auto. rewrite <- to_syn_ok with (1:=Hts2); auto. intros; eapply Ab.thinner_prop; eauto. Qed.
imports: syntax little denot Bool List String ZArith axiom