pred_in_N@{} (n : Graph) (snrec : in_N@{u} (graph_succ n)) : in_N@{u} n. Proof. destruct (N_zero_or_succ (graph_succ n ; snrec)) as [H0|[m Hs]]. - apply pr1_path in H0; cbn in H0. destruct (graph_zero_neq_succ H0^). - apply pr1_path in Hs. apply graph_unsucc_path in Hs. apply (transport@{u p} in_N Hs^). exact m.2. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.