+inductive env_list : nat → Type ≝
+ env_nil: list var_elem → env_list O
+| env_cons: ∀n.list var_elem → env_list n → env_list (S n).
+
+definition defined_envList ≝
+λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ].
+
+definition cut_first_envList : Πd.env_list d → ? → env_list (pred d) ≝
+λd.λl:env_list d.λp:defined_envList ? l.
+ let value ≝
+ match l
+ return λX.λY:env_list X.defined_envList X Y → env_list (pred X)
+ with
+ [ env_nil h ⇒ λp:defined_envList O (env_nil h).False_rect ? p
+ | env_cons n h t ⇒ λp:defined_envList (S n) (env_cons n h t).t
+ ] p in value.
+
+definition get_first_envList ≝
+λd.λl:env_list d.
+ match l with
+ [ env_nil h ⇒ h
+ | env_cons _ h _ ⇒ h
+ ].
+
+lemma defined_envList_S :
+∀d.∀l:env_list (S d).defined_envList (S d) l.
+ intros;
+ inversion l;
+ [ intros; destruct H
+ | intros; simplify; apply I
+ ]
+qed.
+
+definition aux_env_type ≝ λd.env_list d.