我坚持要证明这样的事情。
Theorem EqualContainIn (A: Type) (x: Ensemble A) (y: Ensemble A) (X: Ensemble (Ensemble A)) : forall eq: (Same_set A x y), (X x) -> (X y).
从本质上讲,我希望Same_set
在Ensemble
上被视为判断相等,在Coq中有可能做到这一点吗?
发布于 2018-10-30 18:18:21
明白了,在合奏中有一个Extensionality_Ensembles
公理完全忽略了这一点。但是,有没有可能一种语言直接支持这样的东西,而不是我们将它们定义为一个公理?
https://stackoverflow.com/questions/53061996
复制相似问题