proposition: Lemma equiv_env_item : forall (P : term -> term -> Prop) (n : nat) (e e' : env) (A B : term), item _ A e n -> item _ B e' n -> equiv_env P e e' -> P A B.
proof: Proof. intro P; simple induction n. intros e e' A B H; inversion_clear H. intros H; inversion_clear H; intros H; inversion H; trivial. intros n0 H e e' A B H0; inversion_clear H0. intros H0; inversion_clear H0; intros H0; inversion_clear H0; eauto. Qed.
imports: Termes Conv Ered Types ETypes Conv_Dec Strong_Norm