(* EQUIVALENCE FOR PROTOTERM ************************************************)
+(* Constructions with prototerm_grafted *************************************)
+
+lemma grafted_empty_dx (t):
+ t ⇔ t⋔𝐞.
+/2 width=1 by conj/
+qed.
+
(* Constructions with prototerm_root ****************************************)
lemma prototerm_root_incl_repl: