我有一个函数“ HF”在部分内有类型S
Open S.
HF: forall f : dup_sig Sig, dup_ar f = ASignature.arity (F f)
End S.
Signature: Type
Sig: Signature
dp_Sig : Signature
dup_sig : Signature -> Signature
F : dup_sig Sig -> Sig
dup_symb : Signature -> Type
dup_ar : forall Sig : Signature, dup_symb Sig -> nat
ASignature.arity : forall s : Signature, s -> nat
我想写一个引理：
Lemma incl_fl : forall R R, Fl HF R [= R'.
在哪里
Fl: forall (S1 S2 : Signature) (F : S1 -> S2),
(forall f : S1, ASignature.arity f = ASignature.arity (F f)) ->
list (ATrs.rule S1) -> list (ATrs.rule S2)
当我在 section 中有这个功能时就可以了S。
但我想incl_fl在节外写函数S。这里是HF外节的类型S。
HF: forall (arity : symbol -> nat) (f : dup_sig (Sig arity)),
dup_ar f = ASignature.arity (F f)
Lemma incl_fl : forall arity R R', Fl HF R [= R'.
我在“”处遇到错误HF：
The term "HF" has type
"forall (arity : symbol -> nat) (f : dup_sig (Sig arity)),
dup_ar f = ASignature.arity (F f)" while it is expected to have type
"forall f : ?35524, ASignature.arity f = ASignature.arity (?35526 f)".
我试图找到一个地方arity在这个函数中添加“ HF”，但我没有成功。你能帮我incl_fl在节外写引理“”S吗？非常感谢。