proposition: Lemma thinner_env_prop : forall l l', thinner_env l l' -> forall g, i_a Ab.m g (to_a l) ->i_a Ab.m g (to_a l').
proof: Proof. exact (fun l l' H g => thinner_env_prop_rec l l' H g nil). Qed.
imports: syntax little denot Bool List String ZArith axiom