+
+lemma ple_skip_ple: ∀p. p ≤ ◊ → dx::p ≤ ◊.
+#p #H @(star_ind_l ??????? H) -p //
+#p #q #Hpq #_ #H @(ple_step_sn … H) -H /2 width=1/
+qed.
+
+lemma in_head_ple_nil: ∀p. in_head p → p ≤ ◊.
+#p #H @(in_head_ind … H) -p // /2 width=1/
+qed.
+
+theorem in_head_ple: ∀p. in_head p → ∀q. in_head q → p ≤ q.
+#p #H @(in_head_ind … H) -p //
+#p #Hp #IHp #q #H @(in_head_ind … H) -q /3 width=1/
+qed.
+
+lemma ple_nil_inv_in_head: ∀p. p ≤ ◊ → in_head p.
+#p #H @(star_ind_l ??????? H) -p // /2 width=3 by pprec_fwd_in_head/
+qed-.