proposition: Lemma is_free_ctx_nth_error : forall n m ctx ty, is_free_ctxt n ctx = false -> List.nth_error ctx m = Some ty -> is_free n ty = false.
proof: Proof. unfold is_free_ctxt. intros. assert (is_free n (nth m ctx (Tvar n)) = false). { apply existsb_nth; auto. apply nth_error_Some; congruence. } assert (nth m ctx (Tvar n) = ty) by (apply nth_error_nth; auto). subst; auto. Qed.
imports: List Arith Bool