小编Dha*_*aju的帖子

我为coq中的nat_list的所有子集定义了一个递归函数，如下所示：

Fixpoint subsets (a: list nat) : (list (list nat)) :=
 match a with
  |[] => [[]]
  |h::t => subsets t ++ map (app [h]) (subsets t)
end.

我试图证明

forall (a:list nat), In [] (subsets a).

我试图上一个。基本情况是直接的。但是，在归纳法的情况下，我尝试使用内置定理in_app_or。

Unable to unify "In ?M1396 ?M1394 \/ In ?M1396 ?M1395" with
"(fix In (a : list nat) (l : list (list nat)) {struct l} : Prop := 

match l with
| [] => False
| b :: m => b = …