Coq流共归纳原理证明：mystream_ind引理不满足守卫条件问题

我尝试证明Coq标准库中定义的流谓词的如下原理：

From Coq Require Import Streams.

Lemma mystream_ind :
  forall A (P : Stream A -> Prop),
    (forall s, ForAll P (tl s) -> ForAll P s) ->
    forall s, ForAll P s.
Proof.
  intros A P H.
  cofix Cof.
  destruct s as [a s].
  constructor; auto.
  destruct (H (Cons a s) (Cof s)); auto.
  Fail Guarded.
Abort.

根据我对cofix施加的语法守卫条件的理解，该证明方式无法完成，因为证明项中Cof s必须出现在构造子或者match等守卫结构下，而此处的H不属于符合要求的守卫结构。

疑问 #

请问在Coq中有没有其他实现方案？我还使用paco库将ForAll定义为显式不动点尝试证明该原理，也未成功，完全无法实例化H。

补充说明：该引理实际不可证明，取P := fun s => False时可导出False（感谢Maëlan指出）。

内容的提问来源于stack exchange，提问作者pjm