Consider following mutual inductive proposition

Inductive TypeA : Prop :=
  | ConstructorA : TypeB -> TypeA
with TypeB : Prop :=
  | ConstructorB : TypeA -> TypeB. 

Here is proof of ~TypeA in functional style

Fixpoint TypeA_is_empty' (a : TypeA) : False :=
  match a with 
  | ConstructorA b' => TypeB_is_empty' b'
  end
with TypeB_is_empty' (b : TypeB) : False :=
  match b with 
  | ConstructorB a' => TypeA_is_empty' a'
  end.

How to prove ~TypeA in tactic style?

I want to be able to prove them as mutual Theorems if something similar exists in Coq

Theorem TypeA_is_empty : ~ TypeA.
Theorem TypeB_is_empty : ~ TypeB.
Proof.
  unfold not.
  intros b.
  inversion b as [a].
  apply (TypeA_is_empty a).
Qed.
Proof.
  unfold not.
  intros a.
  inversion a as [b].
  apply (TypeB_is_empty b).
Qed.