小编MJG*_*MJG的帖子

在使用cubical-agda进行一些开发期间，我注意到（后来检查）我当前的目标如果被证明也意味着这样的定理：

parametric? : \xe2\x88\x80 \xe2\x84\x93 \xe2\x86\x92  Type (\xe2\x84\x93-suc \xe2\x84\x93)  \nparametric? \xe2\x84\x93 = (f : {A : Type \xe2\x84\x93} \xe2\x86\x92 List A \xe2\x89\x83 List A)\n                   \xe2\x86\x92 (A : Type \xe2\x84\x93) \xe2\x86\x92 length \xe2\x88\x98 equivFun (f {A}) \xe2\x89\xa1 length\n

我怀疑这是参数定理的例子，这是正确的，但在三次 agda 中无法证明。是这样吗？

我可以放心地假设我当前的目标也是无法证明的吗？