[ { "sort-irrelevant equivalence" * } {
[ [ "" ] "tdeq_ext" + "( ? ≛ ? )" + "( ? ⊢ ? ≛ ? )" * ]
[ [ "" ] "tdeq" + "( ? ≛ ? )" "tdeq_tdeq" * ]
[ { "sort-irrelevant equivalence" * } {
[ [ "" ] "tdeq_ext" + "( ? ≛ ? )" + "( ? ⊢ ? ≛ ? )" * ]
[ [ "" ] "tdeq" + "( ? ≛ ? )" "tdeq_tdeq" * ]