// qed.
(* Main constructions *******************************************************)
theorem height_append (p1) (p2):
// qed.
(* Main constructions *******************************************************)
theorem height_append (p1) (p2):
(* Constructions with list_rcons ********************************************)
lemma height_d_dx (p) (n):
(* Constructions with list_rcons ********************************************)
lemma height_d_dx (p) (n):