+
+definition u0_id (D): u0_fun D D ≝
+ mk_u0_fun D D (u0_i D).
+
+(* Basic properties ***************************************************)
+
+(* auto width 7 in the next lemmas is due to automatic η expansion *)
+lemma u0_class_sym: ∀D. is_u0_class D → u0_sym D (u0_class_in D) (u0_class_eq D).
+#D #HD @u0_refl_repl_sym /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
+
+lemma u0_class_trans: ∀D. is_u0_class D → u0_trans D (u0_class_in D) (u0_class_eq D).
+#D #HD @u0_refl_repl_trans /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
+
+lemma u0_class_conf: ∀D. is_u0_class D → u0_conf D (u0_class_in D) (u0_class_eq D).
+#D #HD @u0_refl_repl_conf /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
+
+lemma u0_class_div: ∀D. is_u0_class D → u0_div D (u0_class_in D) (u0_class_eq D).
+#D #HD @u0_refl_repl_div /2 width=7 by u0_class_repl, u0_class_refl/ qed-.
+
+lemma u0_fun_id: ∀D. is_u0_class D → is_u0_fun D D (u0_id D).
+/2 width=1 by mk_is_u0_fun/ qed.