+(* Basic properties *********************************************************)
+
+lemma tdeq_refl: ∀h,o. reflexive … (tdeq h o).
+#h #o #T elim T -T /2 width=1 by tdeq_pair/
+* /2 width=1 by tdeq_lref, tdeq_gref/
+#s elim (deg_total h o s) /2 width=3 by tdeq_sort/
+qed.
+
+lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o).
+#h #o #T1 #T2 #H elim H -T1 -T2
+/2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/
+qed-.
+