Coq расширяет судейское равенство на ансамбле

Question

Я застрял с доказательством чего-то подобного

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?

Answer 1

Понял, есть аксиома Extensionality_Ensembles в ансамбле, которая полностью пропустила это. Впрочем, возможно ли, чтобы язык непосредственно поддерживал нечто подобное, вместо того, чтобы определять их как аксиому?