proposition: Lemma activeEnv_var_det : forall M x i A, term M = %x -> activeEnv M |= i := A -> i = x /\ A = type M.
proof: Proof. unfold VarD; intros. term_inv M. destruct (lt_eq_lt_dec x0 i) as [[x_lt_i | x_eq_i] | x_gt_i]. rewrite nth_app_right in H0. destruct (O_or_S (i - length (copy x0 (None (A:=SimpleType))))) as [[m sm] | z]. rewrite <- sm in H0; simpl in H0; destruct m; try_solve. absurd (0 = i - length (copy x0 (None (A:=SimpleType)))); trivial. autorewrite with datatypes using lia. autorewrite with datatypes; lia. rewrite x_eq_i in H0. rewrite nth_app_right in H0. replace (i - length (copy i (None (A:=SimpleType)))) with 0 in H0. rewrite <- x_eq_i. replace A0 with A. split; trivial. inversion H; trivial. inversion H0; trivial. autorewrite with datatypes using lia. autorewrite with datatypes using lia. rewrite nth_app_left in H0. rewrite nth_copy_in in H0; try_solve. autorewrite with datatypes using lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsEnv LogicUtil) Coq(Arith Lia)