coq - 帰納的仮定による帰納定理の証明

Question

私は単純な怠惰なバイナリツリーの実装を持っています:

CoInductive LTree (A : Set) : Set :=
| LLeaf : LTree A
| LBin : A -> (LTree A) -> (LTree A) -> LTree A.

そして、次のプロパティ:

(* Having some infinite branch *)

CoInductive SomeInfinite {A} : LTree A -> Prop :=
  SomeInfinite_LBin :
    forall (a : A) (l r : LTree A), (SomeInfinite l \/ SomeInfinite r) ->
      SomeInfinite (LBin _ a l r).

(* Having only finite branches (i.e. being finite) *)

Inductive AllFinite {A} : LTree A -> Prop :=
  | AllFinite_LLeaf : AllFinite (LLeaf A)
  | AllFinite_LBin :
      forall (a : A) (l r : LTree A), (AllFinite l /\ AllFinite r) ->
                                 AllFinite (LBin _ a l r).

有限ツリーには無限分岐がないという定理を証明したいと思います。

Theorem allfinite_noinfinite : forall {A} (t : LTree A), AllFinite t -> not (SomeInfinite t).

...しかし、最初のいくつかの戦術で迷子になりました。仮説自体はかなり些細なことのように思えますが、私はそれから始めることさえできません. そのような定理の証明はどのように見えるでしょうか?