- [ { "degree-based equivalence" * } {
- [ [ "" ] "tdeq_ext" + "( ? ≛[?,?] ? )" + "( ? ⊢ ? ≛[?,?] ? )" * ]
- [ [ "" ] "tdeq" + "( ? ≛[?,?] ? )" "tdeq_tdeq" * ]
+ [ { "sort-irrelevant whd equivalence" * } {
+ [ [ "for terms" ] "teqw" + "( ? ≃ ? )" "teqw_simple" + "teqw_teqg" + "teqw_teqw" * ]
+ }
+ ]
+ [ { "sort-irrelevant equivalence" * } {
+ [ [ "" ] "teqx_ext" + "( ? ≅ ? )" + "( ? ⊢ ? ≅ ? )" * ]
+ [ [ "" ] "teqx" + "( ? ≅ ? )" "teqx_teqx" * ]
+ }
+ ]
+ [ { "syntactic equivalence" * } {
+ [ [ "" ] "teq_ext" + "( ? ≡ ? )" + "( ? ⊢ ? ≡ ? )" "teq_ext_teq_ext" * ]
+ [ [ "" ] "teq" + "( ? ≡ ? )" "teq_teq" * ]
+ }
+ ]
+ [ { "generic equivalence" * } {
+ [ [ "" ] "teqg_ext" + "( ? ≛[?] ? )" + "( ? ⊢ ? ≛[?] ? )" * ]
+ [ [ "" ] "teqg" + "( ? ≛[?] ? )" "teqg_teqg" * ]