proposition: Lemma thinner_env_to_a : forall l1 l2, thinner_env l1 l2 -> forall g, i_a Ab.m g (to_a l1) -> i_a Ab.m g (to_a l2).
proof: Proof. intros l1 l2 Ht g; apply (thinner_env_to_a1 l1 l2 Ht g nil). Qed.
imports: syntax little denot Bool List String ZArith axiom