+
+lemma npred_inj (p): ↓p = ↓(ninj p).
+// qed.
+
+lemma npred_unit: 𝟎 = ↓𝟏.
+// qed.
+
+lemma npred_psucc (p): ninj p = ↓↑p.
+// qed.
+
+(* Basic inversions *********************************************************)
+
+lemma npred_pnat_inv_refl (p): ninj p = ↓p → ⊥.
+*
+[ <npred_unit #H destruct
+| #p /3 width=2 by psucc_inv_refl, eq_inv_ninj_bi/
+]
+qed-.
+
+(*** pred_inv_fix_sn *)
+lemma npred_inv_refl (n): n = ↓n → 𝟎 = n.
+* // #p #H elim (npred_pnat_inv_refl … H)
+qed-.