proposition: Lemma cons_app : forall {a b c} (Γ : env a b) (Δ : env b c) t, cons t (env_app Γ Δ) = env_app Γ (cons t Δ).
proof: Proof. intros. autorewrite with env_app. reflexivity. Qed.
imports: Program Equations(Equations) Coq.Classes.EquivDec Arith