proposition: Lemma no_capture_forall_free : forall n ty1 ty2, no_capture (Forall n ty1) ty2 -> is_free n ty2 = false.
proof: Proof. unfold no_capture; intros n ty1 ty2 H; generalize (H n); simpl. rewrite Nat.eqb_refl; simpl; auto. Qed.
imports: List Arith Bool