コンテキスト内に 2 つの仮説がありますが、1 つの仮説applyを別の仮説にしようとすると、エラーが発生しますunable to unify。私はそれらを統一できるはずです。2つの仮説は次のとおりです。
IHl : forallb func l = true -> All (fun x : X => func x = true) l
H1 : All (fun x : X => func x = true) l
私の目標は、IHl を H1 に適用して、IHl から前提を取得することです。