proposition: Lemma path_finnat_to_fin_incl {n : nat} (u : FinNat n) : finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u).
proof: Proof. induction n as [| n IHn]. - elim (not_lt_n_0 _ u.2). - destruct u as [x h]. destruct x as [| x]; [reflexivity|]. refine ((ap _ (ap _ (path_succ_finnat (x; leq_S_n _ _ h) h)))^ @ _). refine (_ @ ap fsucc (IHn (x; leq_S_n _ _ h))). by induction (path_finnat_to_fin_succ (incl_finnat (x; leq_S_n _ _ h))). Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.Fin