proposition: Lemma thinner_env_trans : forall x y z, thinner_env x y -> thinner_env y z -> thinner_env x z.
proof: Proof. intros x y z H; generalize z; clear z; induction H; intros z Hz; inversion Hz. constructor. constructor; auto. apply Ab.thinner_trans with i2; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom